44 files changed, 1838 insertions, 0 deletions

diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Aggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Aggregator.java
new file mode 100644
index 00000000..47421a94
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Aggregator.java
@@ -0,0 +1,13 @@
+package tools.refinery.store.query.term;
+
+import java.util.stream.Stream;
+
+public interface Aggregator<R, T> {
+        Class<R> getResultType();
+
+        Class<T> getInputType();
+
+        R aggregateStream(Stream<T> stream);
+
+        R getEmptyResult();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java
new file mode 100644
index 00000000..ecfefcf9
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java
@@ -0,0 +1,33 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+
+import java.util.Set;
+
+public abstract sealed class AnyDataVariable extends Variable implements AnyTerm permits DataVariable {
+        protected AnyDataVariable(String name) {
+                super(name);
+        }
+
+        @Override
+        public NodeVariable asNodeVariable() {
+                throw new IllegalStateException("%s is a data variable".formatted(this));
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                return other instanceof AnyDataVariable dataVariable && helper.variableEqual(this, dataVariable);
+        }
+
+        @Override
+        public Set<AnyDataVariable> getInputVariables() {
+                return Set.of(this);
+        }
+
+        @Override
+        public abstract AnyDataVariable renew(@Nullable String name);
+
+        @Override
+        public abstract AnyDataVariable renew();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyTerm.java
new file mode 100644
index 00000000..8f998d45
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyTerm.java
@@ -0,0 +1,16 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+
+import java.util.Set;
+
+public sealed interface AnyTerm permits AnyDataVariable, Term {
+        Class<?> getType();
+
+        AnyTerm substitute(Substitution substitution);
+
+        boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other);
+
+        Set<AnyDataVariable> getInputVariables();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryOperator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryOperator.java
new file mode 100644
index 00000000..8706a046
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryOperator.java
@@ -0,0 +1,26 @@
+package tools.refinery.store.query.term;
+
+public enum ArithmeticBinaryOperator {
+        ADD("+", true),
+        SUB("-", true),
+        MUL("*", true),
+        DIV("/", true),
+        POW("**", true),
+        MIN("min", false),
+        MAX("max", false);
+
+        private final String text;
+        private final boolean infix;
+
+        ArithmeticBinaryOperator(String text, boolean infix) {
+                this.text = text;
+                this.infix = infix;
+        }
+
+        public String formatString(String left, String right) {
+                if (infix) {
+                        return "(%s) %s (%s)".formatted(left, text, right);
+                }
+                return "%s(%s, %s)".formatted(text, left, right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryTerm.java
new file mode 100644
index 00000000..887a1e6e
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryTerm.java
@@ -0,0 +1,56 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+
+import java.util.Objects;
+
+public abstract class ArithmeticBinaryTerm<T> extends BinaryTerm<T, T, T> {
+        private final ArithmeticBinaryOperator operator;
+
+        protected ArithmeticBinaryTerm(ArithmeticBinaryOperator operator, Term<T> left, Term<T> right) {
+                super(left, right);
+                this.operator = operator;
+        }
+
+        @Override
+        public Class<T> getLeftType() {
+                return getType();
+        }
+
+        @Override
+        public Class<T> getRightType() {
+                return getType();
+        }
+
+        public ArithmeticBinaryOperator getOperator() {
+                return operator;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherArithmeticBinaryTerm = (ArithmeticBinaryTerm<?>) other;
+                return operator == otherArithmeticBinaryTerm.operator;
+        }
+
+        @Override
+        public String toString() {
+                return operator.formatString(getLeft().toString(), getRight().toString());
+        }
+
+        @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;
+                ArithmeticBinaryTerm<?> that = (ArithmeticBinaryTerm<?>) o;
+                return operator == that.operator;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), operator);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryOperator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryOperator.java
new file mode 100644
index 00000000..6a7c25db
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryOperator.java
@@ -0,0 +1,16 @@
+package tools.refinery.store.query.term;
+
+public enum ArithmeticUnaryOperator {
+        PLUS("+"),
+        MINUS("-");
+
+        private final String prefix;
+
+        ArithmeticUnaryOperator(String prefix) {
+                this.prefix = prefix;
+        }
+
+        public String formatString(String body) {
+                return "%s(%s)".formatted(prefix, body);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryTerm.java
new file mode 100644
index 00000000..b78239c7
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryTerm.java
@@ -0,0 +1,51 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+
+import java.util.Objects;
+
+public abstract class ArithmeticUnaryTerm<T> extends UnaryTerm<T, T> {
+        private final ArithmeticUnaryOperator operator;
+
+        protected ArithmeticUnaryTerm(ArithmeticUnaryOperator operator, Term<T> body) {
+                super(body);
+                this.operator = operator;
+        }
+
+        @Override
+        public Class<T> getBodyType() {
+                return getType();
+        }
+
+        public ArithmeticUnaryOperator getOperator() {
+                return operator;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherArithmeticUnaryTerm = (ArithmeticUnaryTerm<?>) other;
+                return operator == otherArithmeticUnaryTerm.operator;
+        }
+
+        @Override
+        public String toString() {
+                return operator.formatString(getBody().toString());
+        }
+
+        @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;
+                ArithmeticUnaryTerm<?> that = (ArithmeticUnaryTerm<?>) o;
+                return operator == that.operator;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), operator);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AssignedValue.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AssignedValue.java
new file mode 100644
index 00000000..465e690f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AssignedValue.java
@@ -0,0 +1,8 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.literal.Literal;
+
+@FunctionalInterface
+public interface AssignedValue<T> {
+        Literal toLiteral(DataVariable<T> targetVariable);
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/BinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/BinaryTerm.java
new file mode 100644
index 00000000..34f48ccc
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/BinaryTerm.java
@@ -0,0 +1,93 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.valuation.Valuation;
+
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.Objects;
+import java.util.Set;
+
+public abstract class BinaryTerm<R, T1, T2> implements Term<R> {
+        private final Term<T1> left;
+        private final Term<T2> right;
+
+        protected BinaryTerm(Term<T1> left, Term<T2> right) {
+                if (!left.getType().equals(getLeftType())) {
+                        throw new IllegalArgumentException("Expected left %s to be of type %s, got %s instead".formatted(left,
+                                        getLeftType().getName(), left.getType().getName()));
+                }
+                if (!right.getType().equals(getRightType())) {
+                        throw new IllegalArgumentException("Expected right %s to be of type %s, got %s instead".formatted(right,
+                                        getRightType().getName(), right.getType().getName()));
+                }
+                this.left = left;
+                this.right = right;
+        }
+
+        public abstract Class<T1> getLeftType();
+
+        public abstract Class<T2> getRightType();
+
+        public Term<T1> getLeft() {
+                return left;
+        }
+
+        public Term<T2> getRight() {
+                return right;
+        }
+
+        @Override
+        public R evaluate(Valuation valuation) {
+                var leftValue = left.evaluate(valuation);
+                if (leftValue == null) {
+                        return null;
+                }
+                var rightValue = right.evaluate(valuation);
+                if (rightValue == null) {
+                        return null;
+                }
+                return doEvaluate(leftValue, rightValue);
+        }
+
+        protected abstract R doEvaluate(T1 leftValue, T2 rightValue);
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                if (getClass() != other.getClass()) {
+                        return false;
+                }
+                var otherBinaryTerm = (BinaryTerm<?, ?, ?>) other;
+                return left.equalsWithSubstitution(helper, otherBinaryTerm.left) && right.equalsWithSubstitution(helper,
+                                otherBinaryTerm.right);
+        }
+
+        @Override
+        public Term<R> substitute(Substitution substitution) {
+                return doSubstitute(substitution, left.substitute(substitution), right.substitute(substitution));
+        }
+
+        public abstract Term<R> doSubstitute(Substitution substitution, Term<T1> substitutedLeft,
+                                                                                 Term<T2> substitutedRight);
+
+        @Override
+        public Set<AnyDataVariable> getInputVariables() {
+                var inputVariables = new HashSet<>(left.getInputVariables());
+                inputVariables.addAll(right.getInputVariables());
+                return Collections.unmodifiableSet(inputVariables);
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                BinaryTerm<?, ?, ?> that = (BinaryTerm<?, ?, ?>) o;
+                return left.equals(that.left) && right.equals(that.right);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getClass(), left, right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonOperator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonOperator.java
new file mode 100644
index 00000000..44dcce10
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonOperator.java
@@ -0,0 +1,20 @@
+package tools.refinery.store.query.term;
+
+public enum ComparisonOperator {
+        EQ("=="),
+        NOT_EQ("!="),
+        LESS("<"),
+        LESS_EQ("<="),
+        GREATER(">"),
+        GREATER_EQ(">=");
+
+        private final String text;
+
+        ComparisonOperator(String text) {
+                this.text = text;
+        }
+
+        public String formatString(String left, String right) {
+                return "(%s) %s (%s)".formatted(left, text, right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonTerm.java
new file mode 100644
index 00000000..320d42df
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonTerm.java
@@ -0,0 +1,63 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+
+import java.util.Objects;
+
+public abstract class ComparisonTerm<T> extends BinaryTerm<Boolean, T, T> {
+        private final ComparisonOperator operator;
+
+        protected ComparisonTerm(ComparisonOperator operator, Term<T> left, Term<T> right) {
+                super(left, right);
+                this.operator = operator;
+        }
+
+        @Override
+        public Class<Boolean> getType() {
+                return Boolean.class;
+        }
+
+        public abstract Class<T> getOperandType();
+
+        @Override
+        public Class<T> getLeftType() {
+                return getOperandType();
+        }
+
+        @Override
+        public Class<T> getRightType() {
+                return getOperandType();
+        }
+
+        public ComparisonOperator getOperator() {
+                return operator;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherComparisonTerm = (ComparisonTerm<?>) other;
+                return operator == otherComparisonTerm.operator;
+        }
+
+        @Override
+        public String toString() {
+                return operator.formatString(getLeft().toString(), getRight().toString());
+        }
+
+        @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;
+                ComparisonTerm<?> that = (ComparisonTerm<?>) o;
+                return operator == that.operator;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), operator);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ConstantTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ConstantTerm.java
new file mode 100644
index 00000000..2185fe37
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ConstantTerm.java
@@ -0,0 +1,52 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.valuation.Valuation;
+
+import java.util.Set;
+
+public record ConstantTerm<T>(Class<T> type, T value) implements Term<T> {
+        public ConstantTerm {
+                if (value == null) {
+                        throw new IllegalArgumentException("value should not be null");
+                }
+                if (!type.isInstance(value)) {
+                        throw new IllegalArgumentException("value %s is not an instance of %s".formatted(value, type.getName()));
+                }
+        }
+
+        @Override
+        public Class<T> getType() {
+                return type;
+        }
+
+        public T getValue() {
+                return value;
+        }
+
+        @Override
+        public T evaluate(Valuation valuation) {
+                return getValue();
+        }
+
+        @Override
+        public Term<T> substitute(Substitution substitution) {
+                return this;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                return equals(other);
+        }
+
+        @Override
+        public Set<AnyDataVariable> getInputVariables() {
+                return Set.of();
+        }
+
+        @Override
+        public String toString() {
+                return getValue().toString();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataSort.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataSort.java
new file mode 100644
index 00000000..4fb44492
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataSort.java
@@ -0,0 +1,29 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+
+public record DataSort<T>(Class<T> type) implements Sort {
+        public static final DataSort<Integer> INT = new DataSort<>(Integer.class);
+
+        public static final DataSort<Boolean> BOOL = new DataSort<>(Boolean.class);
+
+        @Override
+        public boolean isInstance(Variable variable) {
+                return variable instanceof DataVariable<?> dataVariable && type.equals(dataVariable.getType());
+        }
+
+        @Override
+        public DataVariable<T> newInstance(@Nullable String name) {
+                return Variable.of(name, type);
+        }
+
+        @Override
+        public DataVariable<T> newInstance() {
+                return newInstance(null);
+        }
+
+        @Override
+        public String toString() {
+                return type.getName();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java
new file mode 100644
index 00000000..af070ca7
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java
@@ -0,0 +1,87 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.valuation.Valuation;
+
+import java.util.Objects;
+
+public final class DataVariable<T> extends AnyDataVariable implements Term<T> {
+        private final Class<T> type;
+
+        DataVariable(String name, Class<T> type) {
+                super(name);
+                this.type = type;
+        }
+
+        @Override
+        public DataSort<T> getSort() {
+                return new DataSort<>(getType());
+        }
+
+        @Override
+        public Class<T> getType() {
+                return type;
+        }
+
+        @Override
+        public DataVariable<T> renew(@Nullable String name) {
+                return new DataVariable<>(name, type);
+        }
+
+        @Override
+        public DataVariable<T> renew() {
+                return renew(getExplicitName());
+        }
+
+        @Override
+        public NodeVariable asNodeVariable() {
+                throw new IllegalStateException("%s is a data variable".formatted(this));
+        }
+
+        @Override
+        public <U> DataVariable<U> asDataVariable(Class<U> newType) {
+                if (!getType().equals(newType)) {
+                        throw new IllegalStateException("%s is not of type %s but of type %s".formatted(this, newType.getName(),
+                                        getType().getName()));
+                }
+                @SuppressWarnings("unchecked")
+                var result = (DataVariable<U>) this;
+                return result;
+        }
+
+        @Override
+        public T evaluate(Valuation valuation) {
+                return valuation.getValue(this);
+        }
+
+        @Override
+        public Term<T> substitute(Substitution substitution) {
+                return substitution.getTypeSafeSubstitute(this);
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                return other instanceof DataVariable<?> dataVariable && helper.variableEqual(this, dataVariable);
+        }
+
+        public Literal assign(AssignedValue<T> value) {
+                return value.toLiteral(this);
+        }
+
+        @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;
+                DataVariable<?> that = (DataVariable<?>) o;
+                return type.equals(that.type);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), type);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ExtremeValueAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ExtremeValueAggregator.java
new file mode 100644
index 00000000..57ff597c
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ExtremeValueAggregator.java
@@ -0,0 +1,103 @@
+package tools.refinery.store.query.term;
+
+import java.util.Comparator;
+import java.util.Objects;
+import java.util.SortedMap;
+import java.util.TreeMap;
+
+public class ExtremeValueAggregator<T> implements StatefulAggregator<T, T> {
+        private final Class<T> type;
+        private final T emptyResult;
+        private final Comparator<T> comparator;
+
+        public ExtremeValueAggregator(Class<T> type, T emptyResult) {
+                this(type, emptyResult, null);
+        }
+
+        public ExtremeValueAggregator(Class<T> type, T emptyResult, Comparator<T> comparator) {
+                this.type = type;
+                this.emptyResult = emptyResult;
+                this.comparator = comparator;
+        }
+
+        @Override
+        public Class<T> getResultType() {
+                return getInputType();
+        }
+
+        @Override
+        public Class<T> getInputType() {
+                return type;
+        }
+
+        @Override
+        public StatefulAggregate<T, T> createEmptyAggregate() {
+                return new Aggregate();
+        }
+
+        @Override
+        public T getEmptyResult() {
+                return emptyResult;
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                ExtremeValueAggregator<?> that = (ExtremeValueAggregator<?>) o;
+                return type.equals(that.type) && Objects.equals(emptyResult, that.emptyResult) && Objects.equals(comparator,
+                                that.comparator);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(type, emptyResult, comparator);
+        }
+
+        private class Aggregate implements StatefulAggregate<T, T> {
+                private final SortedMap<T, Integer> values;
+
+                private Aggregate() {
+                        values = new TreeMap<>(comparator);
+                }
+
+                private Aggregate(Aggregate other) {
+                        values = new TreeMap<>(other.values);
+                }
+
+                @Override
+                public void add(T value) {
+                        values.compute(value, (ignoredValue, currentCount) -> currentCount == null ? 1 : currentCount + 1);
+                }
+
+                @Override
+                public void remove(T value) {
+                        values.compute(value, (theValue, currentCount) -> {
+                                if (currentCount == null || currentCount <= 0) {
+                                        throw new IllegalStateException("Invalid count %d for value %s".formatted(currentCount, theValue));
+                                }
+                                return currentCount.equals(1) ? null : currentCount - 1;
+                        });
+                }
+
+                @Override
+                public T getResult() {
+                        return isEmpty() ? emptyResult : values.firstKey();
+                }
+
+                @Override
+                public boolean isEmpty() {
+                        return values.isEmpty();
+                }
+
+                @Override
+                public StatefulAggregate<T, T> deepCopy() {
+                        return new Aggregate(this);
+                }
+
+                @Override
+                public boolean contains(T value) {
+                        return StatefulAggregate.super.contains(value);
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeSort.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeSort.java
new file mode 100644
index 00000000..1a4b2d4b
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeSort.java
@@ -0,0 +1,30 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+
+public final class NodeSort implements Sort {
+        public static final NodeSort INSTANCE = new NodeSort();
+
+        private NodeSort() {
+        }
+
+        @Override
+        public boolean isInstance(Variable variable) {
+                return variable instanceof NodeVariable;
+        }
+
+        @Override
+        public NodeVariable newInstance(@Nullable String name) {
+                return new NodeVariable(name);
+        }
+
+        @Override
+        public NodeVariable newInstance() {
+                return newInstance(null);
+        }
+
+        @Override
+        public String toString() {
+                return "<node>";
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java
new file mode 100644
index 00000000..7419aaad
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java
@@ -0,0 +1,48 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.query.literal.ConstantLiteral;
+import tools.refinery.store.query.literal.EquivalenceLiteral;
+
+public final class NodeVariable extends Variable {
+        NodeVariable(@Nullable String name) {
+                super(name);
+        }
+
+        @Override
+        public NodeSort getSort() {
+                return NodeSort.INSTANCE;
+        }
+
+        @Override
+        public NodeVariable renew(@Nullable String name) {
+                return Variable.of(name);
+        }
+
+        @Override
+        public NodeVariable renew() {
+                return renew(getExplicitName());
+        }
+
+        @Override
+        public NodeVariable asNodeVariable() {
+                return this;
+        }
+
+        @Override
+        public <T> DataVariable<T> asDataVariable(Class<T> type) {
+                throw new IllegalStateException("%s is a node variable".formatted(this));
+        }
+
+        public ConstantLiteral isConstant(int value) {
+                return new ConstantLiteral(this, value);
+        }
+
+        public EquivalenceLiteral isEquivalent(NodeVariable other) {
+                return new EquivalenceLiteral(true, this, other);
+        }
+
+        public EquivalenceLiteral notEquivalent(NodeVariable other) {
+                return new EquivalenceLiteral(false, this, other);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/OpaqueTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/OpaqueTerm.java
new file mode 100644
index 00000000..8faa9c75
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/OpaqueTerm.java
@@ -0,0 +1,80 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.substitution.Substitutions;
+import tools.refinery.store.query.valuation.Valuation;
+
+import java.util.Objects;
+import java.util.Set;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+public final class OpaqueTerm<T> implements Term<T> {
+        private final Class<T> type;
+        private final Function<? super Valuation, ? extends T> evaluator;
+        private final Set<AnyDataVariable> variables;
+        private final Substitution substitution;
+
+        public OpaqueTerm(Class<T> type, Function<? super Valuation, ? extends T> evaluator,
+                                          Set<? extends AnyDataVariable> variables) {
+                this(type, evaluator, variables, null);
+        }
+
+        private OpaqueTerm(Class<T> type, Function<? super Valuation, ? extends T> evaluator,
+                                           Set<? extends AnyDataVariable> variables, Substitution substitution) {
+                this.type = type;
+                this.evaluator = evaluator;
+                this.variables = Set.copyOf(variables);
+                this.substitution = substitution;
+        }
+
+        @Override
+        public Class<T> getType() {
+                return type;
+        }
+
+        @Override
+        public Set<AnyDataVariable> getInputVariables() {
+                return variables;
+        }
+
+        @Override
+        public T evaluate(Valuation valuation) {
+                return evaluator.apply(valuation.substitute(substitution));
+        }
+
+        @Override
+        public Term<T> substitute(Substitution newSubstitution) {
+                var substitutedVariables = variables.stream()
+                                .map(newSubstitution::getTypeSafeSubstitute)
+                                .collect(Collectors.toUnmodifiableSet());
+                return new OpaqueTerm<>(type, evaluator, substitutedVariables,
+                                Substitutions.compose(substitution, newSubstitution));
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                // Cannot inspect the opaque evaluator for deep equality.
+                return equals(other);
+        }
+
+        @Override
+        public String toString() {
+                return "<opaque>";
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                OpaqueTerm<?> that = (OpaqueTerm<?>) o;
+                return type.equals(that.type) && evaluator.equals(that.evaluator) && Objects.equals(substitution,
+                                that.substitution);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(type, evaluator, substitution);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Sort.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Sort.java
new file mode 100644
index 00000000..622bcfce
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Sort.java
@@ -0,0 +1,11 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+
+public sealed interface Sort permits DataSort, NodeSort {
+        boolean isInstance(Variable variable);
+
+        Variable newInstance(@Nullable String name);
+
+        Variable newInstance();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatefulAggregate.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatefulAggregate.java
new file mode 100644
index 00000000..7ce91305
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatefulAggregate.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.query.term;
+
+public interface StatefulAggregate<R, T> {
+        void add(T value);
+
+        void remove(T value);
+
+        R getResult();
+
+        boolean isEmpty();
+
+        StatefulAggregate<R, T> deepCopy();
+
+        default boolean contains(T value) {
+                throw new UnsupportedOperationException();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatefulAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatefulAggregator.java
new file mode 100644
index 00000000..c215a511
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatefulAggregator.java
@@ -0,0 +1,23 @@
+package tools.refinery.store.query.term;
+
+import java.util.stream.Stream;
+
+public interface StatefulAggregator<R, T> extends Aggregator<R, T> {
+        StatefulAggregate<R, T> createEmptyAggregate();
+
+        @Override
+        default R aggregateStream(Stream<T> stream) {
+                var accumulator = createEmptyAggregate();
+                var iterator = stream.iterator();
+                while (iterator.hasNext()) {
+                        var value = iterator.next();
+                        accumulator.add(value);
+                }
+                return accumulator.getResult();
+        }
+
+        @Override
+        default R getEmptyResult() {
+                return createEmptyAggregate().getResult();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatelessAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatelessAggregator.java
new file mode 100644
index 00000000..74dbd335
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatelessAggregator.java
@@ -0,0 +1,20 @@
+package tools.refinery.store.query.term;
+
+import java.util.stream.Stream;
+
+public interface StatelessAggregator<R, T> extends Aggregator<R, T> {
+        R add(R current, T value);
+
+        R remove(R current, T value);
+
+        @Override
+        default R aggregateStream(Stream<T> stream) {
+                var accumulator = getEmptyResult();
+                var iterator = stream.iterator();
+                while (iterator.hasNext()) {
+                        var value = iterator.next();
+                        accumulator = add(accumulator, value);
+                }
+                return accumulator;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Term.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Term.java
new file mode 100644
index 00000000..95434db2
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Term.java
@@ -0,0 +1,21 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.literal.AssignLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.valuation.Valuation;
+
+public non-sealed interface Term<T> extends AnyTerm, AssignedValue<T> {
+        @Override
+        Class<T> getType();
+
+        T evaluate(Valuation valuation);
+
+        @Override
+        Term<T> substitute(Substitution substitution);
+
+        @Override
+        default Literal toLiteral(DataVariable<T> targetVariable) {
+                return new AssignLiteral<>(targetVariable, this);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/UnaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/UnaryTerm.java
new file mode 100644
index 00000000..4083111a
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/UnaryTerm.java
@@ -0,0 +1,68 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.valuation.Valuation;
+
+import java.util.Objects;
+import java.util.Set;
+
+public abstract class UnaryTerm<R, T> implements Term<R> {
+        private final Term<T> body;
+
+        protected UnaryTerm(Term<T> body) {
+                if (!body.getType().equals(getBodyType())) {
+                        throw new IllegalArgumentException("Expected body %s to be of type %s, got %s instead".formatted(body,
+                                        getBodyType().getName(), body.getType().getName()));
+                }
+                this.body = body;
+        }
+
+        public abstract Class<T> getBodyType();
+
+        public Term<T> getBody() {
+                return body;
+        }
+
+        @Override
+        public R evaluate(Valuation valuation) {
+                var bodyValue = body.evaluate(valuation);
+                return bodyValue == null ? null : doEvaluate(bodyValue);
+        }
+
+        protected abstract R doEvaluate(T bodyValue);
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                if (getClass() != other.getClass()) {
+                        return false;
+                }
+                var otherUnaryTerm = (UnaryTerm<?, ?>) other;
+                return body.equalsWithSubstitution(helper, otherUnaryTerm.body);
+        }
+
+        @Override
+        public Term<R> substitute(Substitution substitution) {
+                return doSubstitute(substitution, body.substitute(substitution));
+        }
+
+        protected abstract Term<R> doSubstitute(Substitution substitution, Term<T> substitutedBody);
+
+        @Override
+        public Set<AnyDataVariable> getInputVariables() {
+                return body.getInputVariables();
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                UnaryTerm<?, ?> unaryTerm = (UnaryTerm<?, ?>) o;
+                return body.equals(unaryTerm.body);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getClass(), body);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java
new file mode 100644
index 00000000..957e10f8
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java
@@ -0,0 +1,76 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.query.dnf.DnfUtils;
+
+import java.util.Objects;
+
+public abstract sealed class Variable permits AnyDataVariable, NodeVariable {
+        private final String explicitName;
+        private final String uniqueName;
+
+        protected Variable(String name) {
+                this.explicitName = name;
+                uniqueName = DnfUtils.generateUniqueName(name);
+        }
+
+        public abstract Sort getSort();
+
+        public String getName() {
+                return explicitName == null ? uniqueName : explicitName;
+        }
+
+        protected String getExplicitName() {
+                return explicitName;
+        }
+
+        public boolean isExplicitlyNamed() {
+                return explicitName != null;
+        }
+
+        public String getUniqueName() {
+                return uniqueName;
+        }
+
+        public abstract Variable renew(@Nullable String name);
+
+        public abstract Variable renew();
+
+        public abstract NodeVariable asNodeVariable();
+
+        public abstract <T> DataVariable<T> asDataVariable(Class<T> type);
+
+        @Override
+        public String toString() {
+                return getName();
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                Variable variable = (Variable) o;
+                return Objects.equals(uniqueName, variable.uniqueName);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(uniqueName);
+        }
+
+        public static NodeVariable of(@Nullable String name) {
+                return new NodeVariable(name);
+        }
+
+        public static NodeVariable of() {
+                return of((String) null);
+        }
+
+        public static <T> DataVariable<T> of(@Nullable String name, Class<T> type) {
+                return new DataVariable<>(name, type);
+        }
+
+        public static <T> DataVariable<T> of(Class<T> type) {
+                return of(null, type);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolConstantTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolConstantTerm.java
new file mode 100644
index 00000000..5079f1ce
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolConstantTerm.java
@@ -0,0 +1,16 @@
+package tools.refinery.store.query.term.bool;
+
+import tools.refinery.store.query.term.ConstantTerm;
+
+public final class BoolConstantTerm {
+        public static final ConstantTerm<Boolean> TRUE = new ConstantTerm<>(Boolean.class, true);
+        public static final ConstantTerm<Boolean> FALSE = new ConstantTerm<>(Boolean.class, false);
+
+        private BoolConstantTerm() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static ConstantTerm<Boolean> valueOf(boolean boolValue) {
+                return boolValue ? TRUE : FALSE;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolLogicBinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolLogicBinaryTerm.java
new file mode 100644
index 00000000..d85f864d
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolLogicBinaryTerm.java
@@ -0,0 +1,78 @@
+package tools.refinery.store.query.term.bool;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.*;
+
+import java.util.Objects;
+
+public class BoolLogicBinaryTerm extends BinaryTerm<Boolean, Boolean, Boolean> {
+        private final LogicBinaryOperator operator;
+
+        protected BoolLogicBinaryTerm(LogicBinaryOperator operator, Term<Boolean> left, Term<Boolean> right) {
+                super(left, right);
+                this.operator = operator;
+        }
+
+        @Override
+        public Class<Boolean> getType() {
+                return Boolean.class;
+        }
+
+        @Override
+        public Class<Boolean> getLeftType() {
+                return getType();
+        }
+
+        @Override
+        public Class<Boolean> getRightType() {
+                return getType();
+        }
+
+        public LogicBinaryOperator getOperator() {
+                return operator;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherBoolLogicBinaryTerm = (BoolLogicBinaryTerm) other;
+                return operator == otherBoolLogicBinaryTerm.operator;
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<Boolean> substitutedLeft,
+                                                                          Term<Boolean> substitutedRight) {
+                return new BoolLogicBinaryTerm(getOperator(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Boolean doEvaluate(Boolean leftValue, Boolean rightValue) {
+                return switch (getOperator()) {
+                        case AND -> leftValue && rightValue;
+                        case OR -> leftValue || rightValue;
+                        case XOR -> leftValue ^ rightValue;
+                };
+        }
+
+        @Override
+        public String toString() {
+                return operator.formatString(getLeft().toString(), getRight().toString());
+        }
+
+        @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;
+                BoolLogicBinaryTerm that = (BoolLogicBinaryTerm) o;
+                return operator == that.operator;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), operator);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolNotTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolNotTerm.java
new file mode 100644
index 00000000..855139b5
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolNotTerm.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.query.term.bool;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.UnaryTerm;
+
+public class BoolNotTerm extends UnaryTerm<Boolean, Boolean> {
+        protected BoolNotTerm(Term<Boolean> body) {
+                super(body);
+        }
+
+        @Override
+        public Class<Boolean> getType() {
+                return Boolean.class;
+        }
+
+        @Override
+        public Class<Boolean> getBodyType() {
+                return getType();
+        }
+
+        @Override
+        protected Term<Boolean> doSubstitute(Substitution substitution, Term<Boolean> substitutedBody) {
+                return new BoolNotTerm(substitutedBody);
+        }
+
+        @Override
+        protected Boolean doEvaluate(Boolean bodyValue) {
+                return !bodyValue;
+        }
+
+        @Override
+        public String toString() {
+                return "!(%s)".formatted(getBody());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolTerms.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolTerms.java
new file mode 100644
index 00000000..3d6c8d9d
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolTerms.java
@@ -0,0 +1,30 @@
+package tools.refinery.store.query.term.bool;
+
+import tools.refinery.store.query.term.ConstantTerm;
+import tools.refinery.store.query.term.Term;
+
+public final class BoolTerms {
+        private BoolTerms() {
+                throw new IllegalArgumentException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static ConstantTerm<Boolean> constant(boolean value) {
+                return BoolConstantTerm.valueOf(value);
+        }
+
+        public static BoolNotTerm not(Term<Boolean> body) {
+                return new BoolNotTerm(body);
+        }
+
+        public static BoolLogicBinaryTerm and(Term<Boolean> left, Term<Boolean> right) {
+                return new BoolLogicBinaryTerm(LogicBinaryOperator.AND, left, right);
+        }
+
+        public static BoolLogicBinaryTerm or(Term<Boolean> left, Term<Boolean> right) {
+                return new BoolLogicBinaryTerm(LogicBinaryOperator.OR, left, right);
+        }
+
+        public static BoolLogicBinaryTerm xor(Term<Boolean> left, Term<Boolean> right) {
+                return new BoolLogicBinaryTerm(LogicBinaryOperator.XOR, left, right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/LogicBinaryOperator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/LogicBinaryOperator.java
new file mode 100644
index 00000000..ca9ac66e
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/LogicBinaryOperator.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.query.term.bool;
+
+public enum LogicBinaryOperator {
+        AND("&&"),
+        OR("||"),
+        XOR("^^");
+
+        private final String text;
+
+        LogicBinaryOperator(String text) {
+                this.text = text;
+        }
+
+        public String formatString(String left, String right) {
+                return "(%s) %s (%s)".formatted(left, text, right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticBinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticBinaryTerm.java
new file mode 100644
index 00000000..32e41718
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticBinaryTerm.java
@@ -0,0 +1,48 @@
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.ArithmeticBinaryOperator;
+import tools.refinery.store.query.term.ArithmeticBinaryTerm;
+import tools.refinery.store.query.term.Term;
+
+public class IntArithmeticBinaryTerm extends ArithmeticBinaryTerm<Integer> {
+        public IntArithmeticBinaryTerm(ArithmeticBinaryOperator operator, Term<Integer> left, Term<Integer> right) {
+                super(operator, left, right);
+        }
+
+        @Override
+        public Class<Integer> getType() {
+                return Integer.class;
+        }
+
+        @Override
+        public Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedLeft,
+                                                                          Term<Integer> substitutedRight) {
+                return new IntArithmeticBinaryTerm(getOperator(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer leftValue, Integer rightValue) {
+                return switch (getOperator()) {
+                        case ADD -> leftValue + rightValue;
+                        case SUB -> leftValue - rightValue;
+                        case MUL -> leftValue * rightValue;
+                        case DIV -> rightValue == 0 ? null : leftValue / rightValue;
+                        case POW -> rightValue < 0 ? null : power(leftValue, rightValue);
+                        case MIN -> Math.min(leftValue, rightValue);
+                        case MAX -> Math.max(leftValue, rightValue);
+                };
+        }
+
+        private static int power(int base, int exponent) {
+                int accum = 1;
+                while (exponent > 0) {
+                        if (exponent % 2 == 1) {
+                                accum = accum * base;
+                        }
+                        base = base * base;
+                        exponent = exponent / 2;
+                }
+                return accum;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticUnaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticUnaryTerm.java
new file mode 100644
index 00000000..1e769259
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticUnaryTerm.java
@@ -0,0 +1,30 @@
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.ArithmeticUnaryOperator;
+import tools.refinery.store.query.term.ArithmeticUnaryTerm;
+
+public class IntArithmeticUnaryTerm extends ArithmeticUnaryTerm<Integer> {
+        public IntArithmeticUnaryTerm(ArithmeticUnaryOperator operation, Term<Integer> body) {
+                super(operation, body);
+        }
+
+        @Override
+        public Class<Integer> getType() {
+                return Integer.class;
+        }
+
+        @Override
+        protected Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedBody) {
+                return new IntArithmeticUnaryTerm(getOperator(), substitutedBody);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer bodyValue) {
+                return switch(getOperator()) {
+                        case PLUS -> bodyValue;
+                        case MINUS -> -bodyValue;
+                };
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntComparisonTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntComparisonTerm.java
new file mode 100644
index 00000000..322d2b80
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntComparisonTerm.java
@@ -0,0 +1,34 @@
+package tools.refinery.store.query.term.int_;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.ComparisonOperator;
+import tools.refinery.store.query.term.ComparisonTerm;
+import tools.refinery.store.query.term.Term;
+
+public class IntComparisonTerm extends ComparisonTerm<Integer> {
+        public IntComparisonTerm(ComparisonOperator operator, Term<Integer> left, Term<Integer> right) {
+                super(operator, left, right);
+        }
+
+        @Override
+        public Class<Integer> getOperandType() {
+                return Integer.class;
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<Integer> substitutedLeft,
+                                                                          Term<Integer> substitutedRight) {
+                return new IntComparisonTerm(getOperator(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Boolean doEvaluate(Integer leftValue, Integer rightValue) {
+                return switch (getOperator()) {
+                        case EQ -> leftValue.equals(rightValue);
+                        case NOT_EQ -> !leftValue.equals(rightValue);
+                        case LESS -> leftValue < rightValue;
+                        case LESS_EQ -> leftValue <= rightValue;
+                        case GREATER -> leftValue > rightValue;
+                        case GREATER_EQ -> leftValue >= rightValue;
+                };
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntExtremeValueAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntExtremeValueAggregator.java
new file mode 100644
index 00000000..d5a6add0
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntExtremeValueAggregator.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.term.ExtremeValueAggregator;
+
+import java.util.Comparator;
+
+public final class IntExtremeValueAggregator {
+        public static final ExtremeValueAggregator<Integer> MINIMUM = new ExtremeValueAggregator<>(Integer.class,
+                        Integer.MAX_VALUE);
+
+        public static final ExtremeValueAggregator<Integer> MAXIMUM = new ExtremeValueAggregator<>(Integer.class,
+                        Integer.MIN_VALUE, Comparator.reverseOrder());
+
+        private IntExtremeValueAggregator() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntSumAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntSumAggregator.java
new file mode 100644
index 00000000..65024f52
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntSumAggregator.java
@@ -0,0 +1,35 @@
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.term.StatelessAggregator;
+
+public final class IntSumAggregator implements StatelessAggregator<Integer, Integer> {
+        public static final IntSumAggregator INSTANCE = new IntSumAggregator();
+
+        private IntSumAggregator() {
+        }
+
+        @Override
+        public Class<Integer> getResultType() {
+                return Integer.class;
+        }
+
+        @Override
+        public Class<Integer> getInputType() {
+                return Integer.class;
+        }
+
+        @Override
+        public Integer getEmptyResult() {
+                return 0;
+        }
+
+        @Override
+        public Integer add(Integer current, Integer value) {
+                return current + value;
+        }
+
+        @Override
+        public Integer remove(Integer current, Integer value) {
+                return current - value;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntTerms.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntTerms.java
new file mode 100644
index 00000000..86594deb
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntTerms.java
@@ -0,0 +1,81 @@
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.term.*;
+
+public final class IntTerms {
+        public static final Aggregator<Integer, Integer> INT_SUM = IntSumAggregator.INSTANCE;
+        public static final Aggregator<Integer, Integer> INT_MIN = IntExtremeValueAggregator.MINIMUM;
+        public static final Aggregator<Integer, Integer> INT_MAX = IntExtremeValueAggregator.MAXIMUM;
+
+        private IntTerms() {
+                throw new IllegalArgumentException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static ConstantTerm<Integer> constant(int value) {
+                return new ConstantTerm<>(Integer.class, value);
+        }
+
+        public static IntArithmeticUnaryTerm plus(Term<Integer> body) {
+                return new IntArithmeticUnaryTerm(ArithmeticUnaryOperator.PLUS, body);
+        }
+
+        public static IntArithmeticUnaryTerm minus(Term<Integer> body) {
+                return new IntArithmeticUnaryTerm(ArithmeticUnaryOperator.MINUS, body);
+        }
+
+        public static IntArithmeticBinaryTerm add(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.ADD, left, right);
+        }
+
+        public static IntArithmeticBinaryTerm sub(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.SUB, left, right);
+        }
+
+        public static IntArithmeticBinaryTerm mul(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.MUL, left, right);
+        }
+
+        public static IntArithmeticBinaryTerm div(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.DIV, left, right);
+        }
+
+        public static IntArithmeticBinaryTerm pow(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.POW, left, right);
+        }
+
+        public static IntArithmeticBinaryTerm min(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.MIN, left, right);
+        }
+
+        public static IntArithmeticBinaryTerm max(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.MAX, left, right);
+        }
+
+        public static IntComparisonTerm eq(Term<Integer> left, Term<Integer> right) {
+                return new IntComparisonTerm(ComparisonOperator.EQ, left, right);
+        }
+
+        public static IntComparisonTerm notEq(Term<Integer> left, Term<Integer> right) {
+                return new IntComparisonTerm(ComparisonOperator.NOT_EQ, left, right);
+        }
+
+        public static IntComparisonTerm less(Term<Integer> left, Term<Integer> right) {
+                return new IntComparisonTerm(ComparisonOperator.LESS, left, right);
+        }
+
+        public static IntComparisonTerm lessEq(Term<Integer> left, Term<Integer> right) {
+                return new IntComparisonTerm(ComparisonOperator.LESS_EQ, left, right);
+        }
+
+        public static IntComparisonTerm greater(Term<Integer> left, Term<Integer> right) {
+                return new IntComparisonTerm(ComparisonOperator.GREATER, left, right);
+        }
+
+        public static IntComparisonTerm greaterEq(Term<Integer> left, Term<Integer> right) {
+                return new IntComparisonTerm(ComparisonOperator.GREATER_EQ, left, right);
+        }
+
+        public static RealToIntTerm asInt(Term<Double> body) {
+                return new RealToIntTerm(body);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/RealToIntTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/RealToIntTerm.java
new file mode 100644
index 00000000..53875ddc
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/RealToIntTerm.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.UnaryTerm;
+
+public class RealToIntTerm extends UnaryTerm<Integer, Double> {
+        protected RealToIntTerm(Term<Double> body) {
+                super(body);
+        }
+
+        @Override
+        public Class<Integer> getType() {
+                return Integer.class;
+        }
+
+        @Override
+        public Class<Double> getBodyType() {
+                return Double.class;
+        }
+
+        @Override
+        protected Integer doEvaluate(Double bodyValue) {
+                return bodyValue.intValue();
+        }
+
+        @Override
+        protected Term<Integer> doSubstitute(Substitution substitution, Term<Double> substitutedBody) {
+                return new RealToIntTerm(substitutedBody);
+        }
+
+        @Override
+        public String toString() {
+                return "(%s) as int".formatted(getBody());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/IntToRealTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/IntToRealTerm.java
new file mode 100644
index 00000000..55590824
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/IntToRealTerm.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.UnaryTerm;
+
+public class IntToRealTerm extends UnaryTerm<Double, Integer> {
+        protected IntToRealTerm(Term<Integer> body) {
+                super(body);
+        }
+
+        @Override
+        public Class<Double> getType() {
+                return Double.class;
+        }
+
+        @Override
+        public Class<Integer> getBodyType() {
+                return Integer.class;
+        }
+
+        @Override
+        protected Term<Double> doSubstitute(Substitution substitution, Term<Integer> substitutedBody) {
+                return new IntToRealTerm(substitutedBody);
+        }
+
+        @Override
+        protected Double doEvaluate(Integer bodyValue) {
+                return bodyValue.doubleValue();
+        }
+
+        @Override
+        public String toString() {
+                return "(%s) as real".formatted(getBody());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticBinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticBinaryTerm.java
new file mode 100644
index 00000000..57bcbe5e
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticBinaryTerm.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.ArithmeticBinaryOperator;
+import tools.refinery.store.query.term.ArithmeticBinaryTerm;
+import tools.refinery.store.query.term.Term;
+
+public class RealArithmeticBinaryTerm extends ArithmeticBinaryTerm<Double> {
+        public RealArithmeticBinaryTerm(ArithmeticBinaryOperator operator, Term<Double> left, Term<Double> right) {
+                super(operator, left, right);
+        }
+
+        @Override
+        public Class<Double> getType() {
+                return Double.class;
+        }
+
+        @Override
+        public Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedLeft,
+                                                                         Term<Double> substitutedRight) {
+                return new RealArithmeticBinaryTerm(getOperator(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Double doEvaluate(Double leftValue, Double rightValue) {
+                return switch (getOperator()) {
+                        case ADD -> leftValue + rightValue;
+                        case SUB -> leftValue - rightValue;
+                        case MUL -> leftValue * rightValue;
+                        case DIV -> leftValue / rightValue;
+                        case POW -> Math.pow(leftValue, rightValue);
+                        case MIN -> Math.min(leftValue, rightValue);
+                        case MAX -> Math.max(leftValue, rightValue);
+                };
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticUnaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticUnaryTerm.java
new file mode 100644
index 00000000..632e68bf
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticUnaryTerm.java
@@ -0,0 +1,30 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.ArithmeticUnaryOperator;
+import tools.refinery.store.query.term.ArithmeticUnaryTerm;
+import tools.refinery.store.query.term.Term;
+
+public class RealArithmeticUnaryTerm extends ArithmeticUnaryTerm<Double> {
+        public RealArithmeticUnaryTerm(ArithmeticUnaryOperator operation, Term<Double> body) {
+                super(operation, body);
+        }
+
+        @Override
+        public Class<Double> getType() {
+                return Double.class;
+        }
+
+        @Override
+        protected Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedBody) {
+                return new RealArithmeticUnaryTerm(getOperator(), substitutedBody);
+        }
+
+        @Override
+        protected Double doEvaluate(Double bodyValue) {
+                return switch(getOperator()) {
+                        case PLUS -> bodyValue;
+                        case MINUS -> -bodyValue;
+                };
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealComparisonTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealComparisonTerm.java
new file mode 100644
index 00000000..75d97adb
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealComparisonTerm.java
@@ -0,0 +1,35 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.ComparisonOperator;
+import tools.refinery.store.query.term.ComparisonTerm;
+import tools.refinery.store.query.term.Term;
+
+public class RealComparisonTerm extends ComparisonTerm<Double> {
+        public RealComparisonTerm(ComparisonOperator operator, Term<Double> left, Term<Double> right) {
+                super(operator, left, right);
+        }
+
+        @Override
+        public Class<Double> getOperandType() {
+                return Double.class;
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<Double> substitutedLeft,
+                                                                          Term<Double> substitutedRight) {
+                return new RealComparisonTerm(getOperator(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Boolean doEvaluate(Double leftValue, Double rightValue) {
+                return switch (getOperator()) {
+                        case EQ -> leftValue.equals(rightValue);
+                        case NOT_EQ -> !leftValue.equals(rightValue);
+                        case LESS -> leftValue < rightValue;
+                        case LESS_EQ -> leftValue <= rightValue;
+                        case GREATER -> leftValue > rightValue;
+                        case GREATER_EQ -> leftValue >= rightValue;
+                };
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealExtremeValueAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealExtremeValueAggregator.java
new file mode 100644
index 00000000..23384530
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealExtremeValueAggregator.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.term.ExtremeValueAggregator;
+
+import java.util.Comparator;
+
+public final class RealExtremeValueAggregator {
+        public static final ExtremeValueAggregator<Double> MINIMUM = new ExtremeValueAggregator<>(Double.class,
+                        Double.POSITIVE_INFINITY);
+
+        public static final ExtremeValueAggregator<Double> MAXIMUM = new ExtremeValueAggregator<>(Double.class,
+                        Double.NEGATIVE_INFINITY, Comparator.reverseOrder());
+
+        private RealExtremeValueAggregator() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealSumAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealSumAggregator.java
new file mode 100644
index 00000000..d5888664
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealSumAggregator.java
@@ -0,0 +1,85 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.term.StatefulAggregate;
+import tools.refinery.store.query.term.StatefulAggregator;
+
+import java.util.Map;
+import java.util.TreeMap;
+
+public final class RealSumAggregator implements StatefulAggregator<Double, Double> {
+        public static final RealSumAggregator INSTANCE = new RealSumAggregator();
+
+        private RealSumAggregator() {
+        }
+
+        @Override
+        public Class<Double> getResultType() {
+                return null;
+        }
+
+        @Override
+        public Class<Double> getInputType() {
+                return null;
+        }
+
+        @Override
+        public StatefulAggregate<Double, Double> createEmptyAggregate() {
+                return new Aggregate();
+        }
+
+        @Override
+        public Double getEmptyResult() {
+                return 0d;
+        }
+
+        private static class Aggregate implements StatefulAggregate<Double, Double> {
+                private final Map<Double, Integer> values;
+
+                public Aggregate() {
+                        values = new TreeMap<>();
+                }
+
+                private Aggregate(Aggregate other) {
+                        values = new TreeMap<>(other.values);
+                }
+
+                @Override
+                public void add(Double value) {
+                        values.compute(value, (ignoredValue, currentCount) -> currentCount == null ? 1 : currentCount + 1);
+                }
+
+                @Override
+                public void remove(Double value) {
+                        values.compute(value, (theValue, currentCount) -> {
+                                if (currentCount == null || currentCount <= 0) {
+                                        throw new IllegalStateException("Invalid count %d for value %f".formatted(currentCount, theValue));
+                                }
+                                return currentCount.equals(1) ? null : currentCount - 1;
+                        });
+                }
+
+                @Override
+                public Double getResult() {
+                        return values.entrySet()
+                                        .stream()
+                                        .mapToDouble(entry -> entry.getKey() * entry.getValue())
+                                        .reduce(Double::sum)
+                                        .orElse(0d);
+                }
+
+                @Override
+                public boolean isEmpty() {
+                        return values.isEmpty();
+                }
+
+                @Override
+                public StatefulAggregate<Double, Double> deepCopy() {
+                        return new Aggregate(this);
+                }
+
+                @Override
+                public boolean contains(Double value) {
+                        return values.containsKey(value);
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealTerms.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealTerms.java
new file mode 100644
index 00000000..a8117842
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealTerms.java
@@ -0,0 +1,81 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.term.*;
+
+public final class RealTerms {
+        public static final Aggregator<Double, Double> REAL_SUM = RealSumAggregator.INSTANCE;
+        public static final Aggregator<Double, Double> REAL_MIN = RealExtremeValueAggregator.MINIMUM;
+        public static final Aggregator<Double, Double> REAL_MAX = RealExtremeValueAggregator.MAXIMUM;
+
+        private RealTerms() {
+                throw new IllegalArgumentException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static ConstantTerm<Double> constant(double value) {
+                return new ConstantTerm<>(Double.class, value);
+        }
+
+        public static RealArithmeticUnaryTerm plus(Term<Double> body) {
+                return new RealArithmeticUnaryTerm(ArithmeticUnaryOperator.PLUS, body);
+        }
+
+        public static RealArithmeticUnaryTerm minus(Term<Double> body) {
+                return new RealArithmeticUnaryTerm(ArithmeticUnaryOperator.MINUS, body);
+        }
+
+        public static RealArithmeticBinaryTerm add(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.ADD, left, right);
+        }
+
+        public static RealArithmeticBinaryTerm sub(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.SUB, left, right);
+        }
+
+        public static RealArithmeticBinaryTerm mul(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.MUL, left, right);
+        }
+
+        public static RealArithmeticBinaryTerm div(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.DIV, left, right);
+        }
+
+        public static RealArithmeticBinaryTerm pow(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.POW, left, right);
+        }
+
+        public static RealArithmeticBinaryTerm min(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.MIN, left, right);
+        }
+
+        public static RealArithmeticBinaryTerm max(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.MAX, left, right);
+        }
+
+        public static RealComparisonTerm eq(Term<Double> left, Term<Double> right) {
+                return new RealComparisonTerm(ComparisonOperator.EQ, left, right);
+        }
+
+        public static RealComparisonTerm notEq(Term<Double> left, Term<Double> right) {
+                return new RealComparisonTerm(ComparisonOperator.NOT_EQ, left, right);
+        }
+
+        public static RealComparisonTerm less(Term<Double> left, Term<Double> right) {
+                return new RealComparisonTerm(ComparisonOperator.LESS, left, right);
+        }
+
+        public static RealComparisonTerm lessEq(Term<Double> left, Term<Double> right) {
+                return new RealComparisonTerm(ComparisonOperator.LESS_EQ, left, right);
+        }
+
+        public static RealComparisonTerm greater(Term<Double> left, Term<Double> right) {
+                return new RealComparisonTerm(ComparisonOperator.GREATER, left, right);
+        }
+
+        public static RealComparisonTerm greaterEq(Term<Double> left, Term<Double> right) {
+                return new RealComparisonTerm(ComparisonOperator.GREATER_EQ, left, right);
+        }
+
+        public static IntToRealTerm asReal(Term<Integer> body) {
+                return new IntToRealTerm(body);
+        }
+}