refactor: DNF query builder

30 files changed, 527 insertions, 376 deletions

diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreImpl.java b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreImpl.java
index b5e1c453..d08cf0f8 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreImpl.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreImpl.java
@@ -1,24 +1,15 @@
 package tools.refinery.store.model;
 
-import java.util.HashMap;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Map;
-import java.util.Map.Entry;
-
-import tools.refinery.store.map.ContinousHashProvider;
-import tools.refinery.store.map.DiffCursor;
-import tools.refinery.store.map.VersionedMap;
-import tools.refinery.store.map.VersionedMapStore;
-import tools.refinery.store.map.VersionedMapStoreImpl;
+import tools.refinery.store.map.*;
 import tools.refinery.store.model.internal.ModelImpl;
 import tools.refinery.store.model.internal.SimilarRelationEquivalenceClass;
-import tools.refinery.store.model.representation.AuxilaryData;
+import tools.refinery.store.model.representation.AuxiliaryData;
 import tools.refinery.store.model.representation.DataRepresentation;
 import tools.refinery.store.model.representation.Relation;
 import tools.refinery.store.tuple.Tuple;
 
-import java.util.Set;
+import java.util.*;
+import java.util.Map.Entry;
 
 public class ModelStoreImpl implements ModelStore {
 
@@ -38,7 +29,7 @@ public class ModelStoreImpl implements ModelStore {
                         if (dataRepresentation instanceof Relation<?> symbolRepresentation) {
                                 addOrCreate(symbolRepresentationsPerHashPerArity,
                                                 new SimilarRelationEquivalenceClass(symbolRepresentation), symbolRepresentation);
-                        } else if (dataRepresentation instanceof AuxilaryData<?, ?>) {
+                        } else if (dataRepresentation instanceof AuxiliaryData<?, ?>) {
                                 VersionedMapStoreImpl<?, ?> store = new VersionedMapStoreImpl<>(dataRepresentation.getHashProvider(),
                                                 dataRepresentation.getDefaultValue());
                                 result.put(dataRepresentation, store);
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/RelationLike.java b/subprojects/store/src/main/java/tools/refinery/store/model/RelationLike.java
new file mode 100644
index 00000000..6a5fdcd5
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/RelationLike.java
@@ -0,0 +1,7 @@
+package tools.refinery.store.model;
+
+public interface RelationLike {
+        String getName();
+
+        int getArity();
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/representation/AuxilaryData.java b/subprojects/store/src/main/java/tools/refinery/store/model/representation/AuxilaryData.java
deleted file mode 100644
index ddd8a5f2..00000000
--- a/subprojects/store/src/main/java/tools/refinery/store/model/representation/AuxilaryData.java
+++ /dev/null
@@ -1,22 +0,0 @@
-package tools.refinery.store.model.representation;
-
-import tools.refinery.store.map.ContinousHashProvider;
-
-public class AuxilaryData<K,V> extends DataRepresentation<K, V> {
-        private final String name;
-
-        public AuxilaryData(String name, ContinousHashProvider<K> hashProvider, V defaultValue) {
-                super(hashProvider, defaultValue);
-                this.name = name;
-        }
-        
-        @Override
-        public String getName() {
-                return name;
-        }
-        
-        @Override
-        public boolean isValidKey(K key) {
-                return true;
-        }
-}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/representation/AuxiliaryData.java b/subprojects/store/src/main/java/tools/refinery/store/model/representation/AuxiliaryData.java
new file mode 100644
index 00000000..1a968f50
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/representation/AuxiliaryData.java
@@ -0,0 +1,22 @@
+package tools.refinery.store.model.representation;
+
+import tools.refinery.store.map.ContinousHashProvider;
+
+public final class AuxiliaryData<K, V> extends DataRepresentation<K, V> {
+        private final ContinousHashProvider<K> hashProvider;
+
+        public AuxiliaryData(String name, ContinousHashProvider<K> hashProvider, V defaultValue) {
+                super(name, defaultValue);
+                this.hashProvider = hashProvider;
+        }
+
+        @Override
+        public ContinousHashProvider<K> getHashProvider() {
+                return hashProvider;
+        }
+
+        @Override
+        public boolean isValidKey(K key) {
+                return true;
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/representation/DataRepresentation.java b/subprojects/store/src/main/java/tools/refinery/store/model/representation/DataRepresentation.java
index 585e7b88..49f74717 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/model/representation/DataRepresentation.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/representation/DataRepresentation.java
@@ -2,20 +2,22 @@ package tools.refinery.store.model.representation;
 
 import tools.refinery.store.map.ContinousHashProvider;
 
-public abstract class DataRepresentation<K, V> {
-        protected final ContinousHashProvider<K> hashProvider;
-        protected final V defaultValue;
+public abstract sealed class DataRepresentation<K, V> permits Relation, AuxiliaryData {
+        private final String name;
 
-        protected DataRepresentation(ContinousHashProvider<K> hashProvider,     V defaultValue) {
-                this.hashProvider = hashProvider;
+        private final V defaultValue;
+
+        protected DataRepresentation(String name, V defaultValue) {
+                this.name = name;
                 this.defaultValue = defaultValue;
         }
-        
-        public abstract String getName();
-        
-        public ContinousHashProvider<K> getHashProvider() {
-                return hashProvider;
+
+        public String getName() {
+                return name;
         }
+
+        public abstract ContinousHashProvider<K> getHashProvider();
+
         public abstract boolean isValidKey(K key);
 
         public V getDefaultValue() {
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/representation/Relation.java b/subprojects/store/src/main/java/tools/refinery/store/model/representation/Relation.java
index c0f31d08..2e21ea37 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/model/representation/Relation.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/representation/Relation.java
@@ -1,31 +1,34 @@
 package tools.refinery.store.model.representation;
 
+import tools.refinery.store.map.ContinousHashProvider;
+import tools.refinery.store.model.RelationLike;
 import tools.refinery.store.tuple.Tuple;
 import tools.refinery.store.model.TupleHashProvider;
 
-public class Relation<D> extends DataRepresentation<Tuple, D> {
-        private final String name;
+public final class Relation<D> extends DataRepresentation<Tuple, D> implements RelationLike {
         private final int arity;
 
         public Relation(String name, int arity, D defaultValue) {
-                super(TupleHashProvider.singleton(), defaultValue);
-                this.name = name;
+                super(name, defaultValue);
                 this.arity = arity;
         }
 
         @Override
-        public String getName() {
-                return name;
-        }
-
         public int getArity() {
                 return arity;
         }
 
         @Override
+        public ContinousHashProvider<Tuple> getHashProvider() {
+                return TupleHashProvider.singleton();
+        }
+
+        @Override
         public boolean isValidKey(Tuple key) {
-                if(key == null) {
+                if (key == null) {
                         return false;
-                } else return key.getSize() == getArity();
+                } else {
+                        return key.getSize() == getArity();
+                }
         }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/DNF.java b/subprojects/store/src/main/java/tools/refinery/store/query/DNF.java
new file mode 100644
index 00000000..7d4b3091
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/DNF.java
@@ -0,0 +1,121 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.model.RelationLike;
+import tools.refinery.store.query.atom.DNFAtom;
+
+import java.util.*;
+
+public class DNF implements RelationLike {
+        private final String name;
+
+        private final String uniqueName;
+
+        private final List<Variable> parameters;
+
+        private final List<DNFAnd> clauses;
+
+        private DNF(String name, List<Variable> parameters, List<DNFAnd> clauses) {
+                this.name = name;
+                this.uniqueName = DNFUtils.generateUniqueName(name);
+                this.parameters = parameters;
+                this.clauses = clauses;
+        }
+
+        @Override
+        public String getName() {
+                return name;
+        }
+
+        public String getUniqueName() {
+                return uniqueName;
+        }
+
+        public List<Variable> getParameters() {
+                return parameters;
+        }
+
+        @Override
+        public int getArity() {
+                return parameters.size();
+        }
+
+        public List<DNFAnd> getClauses() {
+                return clauses;
+        }
+
+        public static Builder builder() {
+                return builder(null);
+        }
+
+        public static Builder builder(String name) {
+                return new Builder(name);
+        }
+
+        @SuppressWarnings("UnusedReturnValue")
+        public static class Builder {
+                private final String name;
+
+                private final List<Variable> parameters = new ArrayList<>();
+
+                private final List<List<DNFAtom>> clauses = new ArrayList<>();
+
+                private Builder(String name) {
+                        this.name = name;
+                }
+
+                public Builder parameter(Variable variable) {
+                        this.parameters.add(variable);
+                        return this;
+                }
+
+                public Builder parameters(Variable... variables) {
+                        return parameters(List.of(variables));
+                }
+
+                public Builder parameters(Collection<Variable> variables) {
+                        this.parameters.addAll(variables);
+                        return this;
+                }
+
+                public Builder clause(DNFAtom... atoms) {
+                        clauses.add(List.of(atoms));
+                        return this;
+                }
+
+                public Builder clause(Collection<DNFAtom> atoms) {
+                        clauses.add(List.copyOf(atoms));
+                        return this;
+                }
+
+                public Builder clause(DNFAnd clause) {
+                        return clause(clause.constraints());
+                }
+
+                public Builder clauses(DNFAnd... clauses) {
+                        for (var clause : clauses) {
+                                this.clause(clause);
+                        }
+                        return this;
+                }
+
+                public Builder clauses(Collection<DNFAnd> clauses) {
+                        for (var clause : clauses) {
+                                this.clause(clause);
+                        }
+                        return this;
+                }
+
+                public DNF build() {
+                        var postProcessedClauses = new ArrayList<DNFAnd>();
+                        for (var constraints : clauses) {
+                                var variables = new HashSet<Variable>();
+                                for (var constraint : constraints) {
+                                        constraint.collectAllVariables(variables);
+                                }
+                                parameters.forEach(variables::remove);
+                                postProcessedClauses.add(new DNFAnd(variables, constraints));
+                        }
+                        return new DNF(name, List.copyOf(parameters), postProcessedClauses);
+                }
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/DNFAnd.java b/subprojects/store/src/main/java/tools/refinery/store/query/DNFAnd.java
new file mode 100644
index 00000000..8c3bf05d
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/DNFAnd.java
@@ -0,0 +1,9 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.query.atom.DNFAtom;
+
+import java.util.List;
+import java.util.Set;
+
+public record DNFAnd(Set<Variable> quantifiedVariables, List<DNFAtom> constraints) {
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/DNFUtils.java b/subprojects/store/src/main/java/tools/refinery/store/query/DNFUtils.java
new file mode 100644
index 00000000..0ef77d49
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/DNFUtils.java
@@ -0,0 +1,19 @@
+package tools.refinery.store.query;
+
+import java.util.UUID;
+
+public final class DNFUtils {
+        private DNFUtils() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static String generateUniqueName(String originalName) {
+                UUID uuid = UUID.randomUUID();
+                String uniqueString = "_" + uuid.toString().replace('-', '_');
+                if (originalName == null) {
+                        return uniqueString;
+                } else {
+                        return originalName + uniqueString;
+                }
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/QueryableModel.java b/subprojects/store/src/main/java/tools/refinery/store/query/QueryableModel.java
index 648c3a36..9655d1a1 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/QueryableModel.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/QueryableModel.java
@@ -1,7 +1,6 @@
 package tools.refinery.store.query;
 
 import tools.refinery.store.model.Model;
-import tools.refinery.store.query.building.DNFPredicate;
 import tools.refinery.store.tuple.Tuple;
 import tools.refinery.store.tuple.TupleLike;
 
@@ -10,25 +9,25 @@ import java.util.Set;
 import java.util.stream.Stream;
 
 public interface QueryableModel extends Model {
-        Set<DNFPredicate> getPredicates();
+        Set<DNF> getPredicates();
 
         boolean hasChanges();
 
         void flushChanges();
 
-        boolean hasResult(DNFPredicate predicate);
+        boolean hasResult(DNF predicate);
 
-        boolean hasResult(DNFPredicate predicate, Tuple parameters);
+        boolean hasResult(DNF predicate, Tuple parameters);
 
-        Optional<TupleLike> oneResult(DNFPredicate predicate);
+        Optional<TupleLike> oneResult(DNF predicate);
 
-        Optional<TupleLike> oneResult(DNFPredicate predicate, Tuple parameters);
+        Optional<TupleLike> oneResult(DNF predicate, Tuple parameters);
 
-        Stream<TupleLike> allResults(DNFPredicate predicate);
+        Stream<TupleLike> allResults(DNF predicate);
 
-        Stream<TupleLike> allResults(DNFPredicate predicate, Tuple parameters);
+        Stream<TupleLike> allResults(DNF predicate, Tuple parameters);
 
-        int countResults(DNFPredicate predicate);
+        int countResults(DNF predicate);
 
-        int countResults(DNFPredicate predicate, Tuple parameters);
+        int countResults(DNF predicate, Tuple parameters);
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/QueryableModelStore.java b/subprojects/store/src/main/java/tools/refinery/store/query/QueryableModelStore.java
index 878e1058..41f47e64 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/QueryableModelStore.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/QueryableModelStore.java
@@ -2,7 +2,6 @@ package tools.refinery.store.query;
 
 import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.model.representation.DataRepresentation;
-import tools.refinery.store.query.building.DNFPredicate;
 import tools.refinery.store.query.view.RelationView;
 
 import java.util.Set;
@@ -14,7 +13,7 @@ public interface QueryableModelStore extends ModelStore {
         @SuppressWarnings("squid:S1452")
         Set<RelationView<?>> getViews();
 
-        Set<DNFPredicate> getPredicates();
+        Set<DNF> getPredicates();
 
         QueryableModel createModel();
 
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java b/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java
new file mode 100644
index 00000000..3632f3c5
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java
@@ -0,0 +1,43 @@
+package tools.refinery.store.query;
+
+import java.util.Objects;
+
+public class Variable {
+        private final String name;
+        private final String uniqueName;
+
+        public Variable() {
+                this(null);
+        }
+
+        public Variable(String name) {
+                super();
+                this.name = name;
+                this.uniqueName = DNFUtils.generateUniqueName(name);
+
+        }
+        public String getName() {
+                return name;
+        }
+
+        public String getUniqueName() {
+                return uniqueName;
+        }
+
+        public boolean isNamed() {
+                return name != null;
+        }
+
+        @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);
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/atom/AbstractCallAtom.java b/subprojects/store/src/main/java/tools/refinery/store/query/atom/AbstractCallAtom.java
new file mode 100644
index 00000000..fb8d7432
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/atom/AbstractCallAtom.java
@@ -0,0 +1,30 @@
+package tools.refinery.store.query.atom;
+
+import tools.refinery.store.model.RelationLike;
+import tools.refinery.store.query.Variable;
+
+import java.util.List;
+import java.util.Set;
+
+public abstract class AbstractCallAtom<T extends RelationLike> extends AbstractSubstitutionAtom<T> {
+        private final CallKind kind;
+
+        protected AbstractCallAtom(CallKind kind, T target, List<Variable> substitution) {
+                super(target, substitution);
+                if (kind.isTransitive() && target.getArity() != 2) {
+                        throw new IllegalArgumentException("Transitive closures can only take binary relations");
+                }
+                this.kind = kind;
+        }
+
+        public CallKind getKind() {
+                return kind;
+        }
+
+        @Override
+        public void collectAllVariables(Set<Variable> variables) {
+                if (kind.isPositive()) {
+                        super.collectAllVariables(variables);
+                }
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/atom/AbstractSubstitutionAtom.java b/subprojects/store/src/main/java/tools/refinery/store/query/atom/AbstractSubstitutionAtom.java
new file mode 100644
index 00000000..e8a8b5e1
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/atom/AbstractSubstitutionAtom.java
@@ -0,0 +1,35 @@
+package tools.refinery.store.query.atom;
+
+import tools.refinery.store.model.RelationLike;
+import tools.refinery.store.query.Variable;
+
+import java.util.List;
+import java.util.Set;
+
+public abstract class AbstractSubstitutionAtom<T extends RelationLike> implements DNFAtom {
+        private final T target;
+
+        private final List<Variable> substitution;
+
+        protected AbstractSubstitutionAtom(T target, List<Variable> substitution) {
+                if (substitution.size() != target.getArity()) {
+                        throw new IllegalArgumentException("%s needs %d arguments, but got %s".formatted(target.getName(),
+                                        target.getArity(), substitution.size()));
+                }
+                this.target = target;
+                this.substitution = substitution;
+        }
+
+        public T getTarget() {
+                return target;
+        }
+
+        public List<Variable> getSubstitution() {
+                return substitution;
+        }
+
+        @Override
+        public void collectAllVariables(Set<Variable> variables) {
+                variables.addAll(substitution);
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/atom/CallKind.java b/subprojects/store/src/main/java/tools/refinery/store/query/atom/CallKind.java
new file mode 100644
index 00000000..c7cbc955
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/atom/CallKind.java
@@ -0,0 +1,24 @@
+package tools.refinery.store.query.atom;
+
+public enum CallKind {
+        POSITIVE(true, false),
+        NEGATIVE(false, false),
+        TRANSITIVE(true, true);
+
+        private final boolean positive;
+
+        private final boolean transitive;
+
+        CallKind(boolean positive, boolean transitive) {
+                this.positive = positive;
+                this.transitive = transitive;
+        }
+
+        public boolean isPositive() {
+                return positive;
+        }
+
+        public boolean isTransitive() {
+                return transitive;
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/atom/DNFAtom.java b/subprojects/store/src/main/java/tools/refinery/store/query/atom/DNFAtom.java
new file mode 100644
index 00000000..ebf71236
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/atom/DNFAtom.java
@@ -0,0 +1,9 @@
+package tools.refinery.store.query.atom;
+
+import tools.refinery.store.query.Variable;
+
+import java.util.Set;
+
+public interface DNFAtom {
+        void collectAllVariables(Set<Variable> variables);
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/atom/DNFCallAtom.java b/subprojects/store/src/main/java/tools/refinery/store/query/atom/DNFCallAtom.java
new file mode 100644
index 00000000..9d2efa53
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/atom/DNFCallAtom.java
@@ -0,0 +1,40 @@
+package tools.refinery.store.query.atom;
+
+import tools.refinery.store.query.DNF;
+import tools.refinery.store.query.Variable;
+
+import java.util.List;
+import java.util.Objects;
+
+public final class DNFCallAtom extends AbstractCallAtom<DNF> {
+        public DNFCallAtom(CallKind kind, DNF target, List<Variable> substitution) {
+                super(kind, target, substitution);
+        }
+
+        public DNFCallAtom(CallKind kind, DNF target, Variable... substitution) {
+                super(kind, target, List.of(substitution));
+        }
+
+        public DNFCallAtom(DNF target, List<Variable> substitution) {
+                this(CallKind.POSITIVE, target, substitution);
+        }
+
+        public DNFCallAtom(DNF target, Variable... substitution) {
+                this(target, List.of(substitution));
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                DNFCallAtom dnfCallAtom = (DNFCallAtom) o;
+                return Objects.equals(getKind(), dnfCallAtom.getKind())
+                                && Objects.equals(getTarget(), dnfCallAtom.getTarget())
+                                && Objects.equals(getSubstitution(), dnfCallAtom.getSubstitution());
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getKind(), getTarget(), getSubstitution());
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/atom/EquivalenceAtom.java b/subprojects/store/src/main/java/tools/refinery/store/query/atom/EquivalenceAtom.java
new file mode 100644
index 00000000..b1b3a6f7
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/atom/EquivalenceAtom.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.query.atom;
+
+import tools.refinery.store.query.Variable;
+
+import java.util.Set;
+
+public record EquivalenceAtom(boolean positive, Variable left, Variable right) implements DNFAtom {
+        public EquivalenceAtom(Variable left, Variable right) {
+                this(true, left, right);
+        }
+
+        @Override
+        public void collectAllVariables(Set<Variable> variables) {
+                variables.add(left);
+                variables.add(right);
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/atom/ModalRelationAtom.java b/subprojects/store/src/main/java/tools/refinery/store/query/atom/ModalRelationAtom.java
new file mode 100644
index 00000000..2480e82e
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/atom/ModalRelationAtom.java
@@ -0,0 +1,38 @@
+package tools.refinery.store.query.atom;
+
+import tools.refinery.store.model.representation.Relation;
+import tools.refinery.store.model.representation.TruthValue;
+import tools.refinery.store.query.Variable;
+
+import java.util.List;
+import java.util.Objects;
+
+public final class ModalRelationAtom extends AbstractCallAtom<Relation<TruthValue>> {
+        private final Modality modality;
+
+        public ModalRelationAtom(CallKind kind, Modality modality, Relation<TruthValue> target,
+                                                         List<Variable> substitution) {
+                super(kind, target, substitution);
+                this.modality = modality;
+        }
+
+        public ModalRelationAtom(Modality modality, Relation<TruthValue> target, List<Variable> substitution) {
+                this(CallKind.POSITIVE, modality, target, substitution);
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                ModalRelationAtom modalRelationAtom = (ModalRelationAtom) o;
+                return Objects.equals(getKind(), modalRelationAtom.getKind())
+                                && modality == modalRelationAtom.modality
+                                && Objects.equals(getTarget(), modalRelationAtom.getTarget())
+                                && Objects.equals(getSubstitution(), modalRelationAtom.getSubstitution());
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getKind(), modality, getTarget(), getSubstitution());
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/atom/Modality.java b/subprojects/store/src/main/java/tools/refinery/store/query/atom/Modality.java
new file mode 100644
index 00000000..9344a9d3
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/atom/Modality.java
@@ -0,0 +1,7 @@
+package tools.refinery.store.query.atom;
+
+public enum Modality {
+        MUST,
+        MAY,
+        CURRENT;
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/atom/RelationAtom.java b/subprojects/store/src/main/java/tools/refinery/store/query/atom/RelationAtom.java
new file mode 100644
index 00000000..06098139
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/atom/RelationAtom.java
@@ -0,0 +1,32 @@
+package tools.refinery.store.query.atom;
+
+import tools.refinery.store.model.representation.Relation;
+import tools.refinery.store.query.Variable;
+
+import java.util.List;
+import java.util.Objects;
+
+public final class RelationAtom extends AbstractCallAtom<Relation<?>> {
+        public RelationAtom(CallKind kind, Relation<?> target, List<Variable> substitution) {
+                super(kind, target, substitution);
+        }
+
+        public RelationAtom(Relation<?> target, List<Variable> substitution) {
+                this(CallKind.POSITIVE, target, substitution);
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                RelationAtom relationAtom = (RelationAtom) o;
+                return Objects.equals(getKind(), relationAtom.getKind())
+                                && Objects.equals(getTarget(), relationAtom.getTarget())
+                                && Objects.equals(getSubstitution(), relationAtom.getSubstitution());
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getKind(), getTarget(), getSubstitution());
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/atom/RelationViewAtom.java b/subprojects/store/src/main/java/tools/refinery/store/query/atom/RelationViewAtom.java
new file mode 100644
index 00000000..762a41f1
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/atom/RelationViewAtom.java
@@ -0,0 +1,31 @@
+package tools.refinery.store.query.atom;
+
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.view.RelationView;
+
+import java.util.List;
+import java.util.Objects;
+
+public final class RelationViewAtom extends AbstractSubstitutionAtom<RelationView<?>> {
+        public RelationViewAtom(RelationView<?> target, List<Variable> substitution) {
+                super(target, substitution);
+        }
+
+        public RelationViewAtom(RelationView<?> target, Variable... substitution) {
+                this(target, List.of(substitution));
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                RelationViewAtom relationViewAtom = (RelationViewAtom) o;
+                return Objects.equals(getTarget(), relationViewAtom.getTarget())
+                                && Objects.equals(getSubstitution(), relationViewAtom.getSubstitution());
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getTarget(), getSubstitution());
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/building/DNFAnd.java b/subprojects/store/src/main/java/tools/refinery/store/query/building/DNFAnd.java
deleted file mode 100644
index 48dabce2..00000000
--- a/subprojects/store/src/main/java/tools/refinery/store/query/building/DNFAnd.java
+++ /dev/null
@@ -1,37 +0,0 @@
-package tools.refinery.store.query.building;
-
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.List;
-import java.util.Map;
-import java.util.Set;
-
-public class DNFAnd {
-        private Set<Variable> existentiallyQuantified;
-        private List<DNFAtom> constraints;
-        public DNFAnd(Set<Variable> quantifiedVariables, List<DNFAtom> constraints) {
-                super();
-                this.existentiallyQuantified = quantifiedVariables;
-                this.constraints = constraints;
-        }
-        public Set<Variable> getExistentiallyQuantified() {
-                return existentiallyQuantified;
-        }
-        public List<DNFAtom> getConstraints() {
-                return constraints;
-        }
-        void unifyVariables(Map<String,Variable> uniqueVariableMap) {
-                Map<String,Variable> uniqueVariableMapForClause = new HashMap<>(uniqueVariableMap);
-                for(DNFAtom atom : constraints) {
-                        atom.unifyVariables(uniqueVariableMapForClause);
-                }
-        }
-        void collectQuantifiedVariables(Set<Variable> parameters) {
-                Set<Variable> result = new HashSet<>();
-                for(DNFAtom constraint : constraints) {
-                        constraint.collectAllVariables(result);
-                }
-                result.removeAll(parameters);
-                existentiallyQuantified = result;
-        }
-}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/building/DNFAtom.java b/subprojects/store/src/main/java/tools/refinery/store/query/building/DNFAtom.java
deleted file mode 100644
index b047d7c8..00000000
--- a/subprojects/store/src/main/java/tools/refinery/store/query/building/DNFAtom.java
+++ /dev/null
@@ -1,33 +0,0 @@
-package tools.refinery.store.query.building;
-
-import java.util.Collection;
-import java.util.Iterator;
-import java.util.Map;
-import java.util.Set;
-
-public interface DNFAtom {
-        void unifyVariables(Map<String,Variable> variables);
-        static Variable unifyVariables(Map<String,Variable> unifiedVariables, Variable variable) {
-                if(variable != null) {
-                        if(variable.isNamed() && unifiedVariables.containsKey(variable.getName())) {
-                                return unifiedVariables.get(variable.getName());
-                        }
-                        return variable;
-                } else {
-                        return null;
-                }
-        }
-        void collectAllVariables(Set<Variable> variables);
-        static void addToCollection(Set<Variable> variables, Variable variable) {
-                if(variable != null) {
-                        variables.add(variable);
-                }
-        }
-        static void addToCollection(Set<Variable> variables, Collection<Variable> variableCollection) {
-                Iterator<Variable> iterator = variableCollection.iterator();
-                while(iterator.hasNext()) {
-                        Variable variable = iterator.next();
-                        addToCollection(variables, variable);
-                }
-        }
-}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/building/DNFPredicate.java b/subprojects/store/src/main/java/tools/refinery/store/query/building/DNFPredicate.java
deleted file mode 100644
index f0c9ac42..00000000
--- a/subprojects/store/src/main/java/tools/refinery/store/query/building/DNFPredicate.java
+++ /dev/null
@@ -1,72 +0,0 @@
-package tools.refinery.store.query.building;
-
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.List;
-import java.util.Map;
-import java.util.UUID;
-
-public class DNFPredicate {
-        private final String name;
-        private final String uniqueName;
-        private final List<Variable> parameters;
-        private final List<DNFAnd> clauses;
-        
-        public DNFPredicate(String name, List<Variable> parameters, List<DNFAnd> clauses) {
-                this.name = name;
-                this.uniqueName = generateUniqueName(name,"predicate");
-                this.parameters = parameters;
-                this.clauses = clauses;
-                
-                postProcess();
-        }
-        
-        public static String generateUniqueName(String originalName, String defaultPrefix) {
-                UUID uuid = UUID.randomUUID();
-                String uniqueString = uuid.toString().replace('-', '_');
-                if(originalName == null) {
-                        return defaultPrefix+uniqueString;
-                } else {
-                        return originalName+uniqueString;
-                }
-        }
-        
-        public String getName() {
-                return name;
-        }
-        public String getUniqueName() {
-                return uniqueName;
-        }
-        public List<Variable> getVariables() {
-                return parameters;
-        }
-        public List<DNFAnd> getClauses() {
-                return clauses;
-        }
-        
-        public void unifyVariables() {
-                Map<String,Variable> uniqueVariableMap = new HashMap<>();
-                for(Variable parameter : this.parameters) {
-                        if(parameter.isNamed()) {
-                                String parameterName = parameter.getName();
-                                if(uniqueVariableMap.containsKey(parameterName)) {
-                                        throw new IllegalArgumentException("Multiple parameters has the name "+parameterName);
-                                } else {
-                                        uniqueVariableMap.put(parameterName, parameter);
-                                }
-                        }
-                }
-                for(DNFAnd clause : this.clauses) {
-                        clause.unifyVariables(uniqueVariableMap);
-                }
-        }
-        public void collectQuantifiedVariables() {
-                for(DNFAnd clause : this.clauses) {
-                        clause.collectQuantifiedVariables(new HashSet<>(parameters));
-                }
-        }
-        public void postProcess() {
-                unifyVariables();
-                collectQuantifiedVariables();
-        }
-}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/building/EquivalenceAtom.java b/subprojects/store/src/main/java/tools/refinery/store/query/building/EquivalenceAtom.java
deleted file mode 100644
index fede2518..00000000
--- a/subprojects/store/src/main/java/tools/refinery/store/query/building/EquivalenceAtom.java
+++ /dev/null
@@ -1,44 +0,0 @@
-package tools.refinery.store.query.building;
-
-import java.util.Map;
-import java.util.Set;
-
-public class EquivalenceAtom implements DNFAtom{
-        private boolean positive;
-        private Variable left;
-        private Variable right;
-        public EquivalenceAtom(boolean positive, Variable left, Variable right) {
-                this.positive = positive;
-                this.left = left;
-                this.right = right;
-        }
-        public boolean isPositive() {
-                return positive;
-        }
-        public void setPositive(boolean positive) {
-                this.positive = positive;
-        }
-        public Variable getLeft() {
-                return left;
-        }
-        public void setLeft(Variable left) {
-                this.left = left;
-        }
-        public Variable getRight() {
-                return right;
-        }
-        public void setRight(Variable right) {
-                this.right = right;
-        }
-        
-        @Override
-        public void unifyVariables(Map<String, Variable> variables) {
-                this.left = DNFAtom.unifyVariables(variables,left);
-                this.right = DNFAtom.unifyVariables(variables,right);
-        }
-        @Override
-        public void collectAllVariables(Set<Variable> variables) {
-                DNFAtom.addToCollection(variables, left);
-                DNFAtom.addToCollection(variables, right);
-        }
-}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/building/PredicateAtom.java b/subprojects/store/src/main/java/tools/refinery/store/query/building/PredicateAtom.java
deleted file mode 100644
index 42394922..00000000
--- a/subprojects/store/src/main/java/tools/refinery/store/query/building/PredicateAtom.java
+++ /dev/null
@@ -1,66 +0,0 @@
-package tools.refinery.store.query.building;
-
-import java.util.List;
-import java.util.Map;
-import java.util.Set;
-
-public class PredicateAtom implements DNFAtom {
-        private DNFPredicate referred;
-        private List<Variable> substitution;
-        private boolean positive;
-        private boolean transitive;
-
-        public PredicateAtom(boolean positive, boolean transitive, DNFPredicate referred, List<Variable> substitution) {
-                this.positive = positive;
-                this.referred = referred;
-                this.substitution = substitution;
-                this.transitive = transitive;
-        }
-
-        public DNFPredicate getReferred() {
-                return referred;
-        }
-
-        public void setReferred(DNFPredicate referred) {
-                this.referred = referred;
-        }
-
-        public List<Variable> getSubstitution() {
-                return substitution;
-        }
-
-        public void setSubstitution(List<Variable> substitution) {
-                this.substitution = substitution;
-        }
-
-        public boolean isPositive() {
-                return positive;
-        }
-
-        public void setPositive(boolean positive) {
-                this.positive = positive;
-        }
-
-        public boolean isTransitive() {
-                return transitive;
-        }
-
-        public void setTransitive(boolean transitive) {
-                this.transitive = transitive;
-        }
-
-        @Override
-        public void unifyVariables(Map<String, Variable> variables) {
-                for (int i = 0; i < this.substitution.size(); i++) {
-                        final Object term = this.substitution.get(i);
-                        if (term instanceof Variable variableReference) {
-                                this.substitution.set(i, DNFAtom.unifyVariables(variables, variableReference));
-                        }
-                }
-        }
-
-        @Override
-        public void collectAllVariables(Set<Variable> variables) {
-                DNFAtom.addToCollection(variables, substitution);
-        }
-}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/building/RelationAtom.java b/subprojects/store/src/main/java/tools/refinery/store/query/building/RelationAtom.java
deleted file mode 100644
index f66245fc..00000000
--- a/subprojects/store/src/main/java/tools/refinery/store/query/building/RelationAtom.java
+++ /dev/null
@@ -1,31 +0,0 @@
-package tools.refinery.store.query.building;
-
-import tools.refinery.store.query.view.RelationView;
-
-import java.util.ArrayList;
-import java.util.List;
-import java.util.Map;
-import java.util.Set;
-
-public record RelationAtom(RelationView<?> view, List<Variable> substitution) implements DNFAtom {
-        public RelationAtom(RelationView<?> view, List<Variable> substitution) {
-                this.view = view;
-                // Create a mutable copy of substitution so that unifyVariables can change it.
-                this.substitution = new ArrayList<>(substitution);
-        }
-
-        @Override
-        public void unifyVariables(Map<String, Variable> variables) {
-                for (int i = 0; i < this.substitution.size(); i++) {
-                        final Object term = this.substitution.get(i);
-                        if (term instanceof Variable variableReference) {
-                                this.substitution.set(i, DNFAtom.unifyVariables(variables, variableReference));
-                        }
-                }
-        }
-
-        @Override
-        public void collectAllVariables(Set<Variable> variables) {
-                DNFAtom.addToCollection(variables, substitution);
-        }
-}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/building/Variable.java b/subprojects/store/src/main/java/tools/refinery/store/query/building/Variable.java
deleted file mode 100644
index 9ea7ce83..00000000
--- a/subprojects/store/src/main/java/tools/refinery/store/query/building/Variable.java
+++ /dev/null
@@ -1,22 +0,0 @@
-package tools.refinery.store.query.building;
-
-public class Variable {
-        private final String name;
-        private final String uniqueName;
-
-        public Variable(String name) {
-                super();
-                this.name = name;
-                this.uniqueName = DNFPredicate.generateUniqueName(name, "variable");
-                
-        }
-        public String getName() {
-                return name;
-        }
-        public String getUniqueName() {
-                return uniqueName;
-        }
-        public boolean isNamed() {
-                return name != null;
-        }
-}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java
index ceaf7d55..96f8584a 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java
@@ -2,6 +2,7 @@ package tools.refinery.store.query.view;
 
 import tools.refinery.store.map.CursorAsIterator;
 import tools.refinery.store.model.Model;
+import tools.refinery.store.model.RelationLike;
 import tools.refinery.store.tuple.Tuple;
 import tools.refinery.store.model.representation.Relation;
 
@@ -14,7 +15,7 @@ import java.util.UUID;
  * @param <D>
  * @author Oszkar Semerath
  */
-public abstract class RelationView<D> {
+public abstract class RelationView<D> implements RelationLike {
         private final Relation<D> representation;
 
         private final String name;
@@ -28,12 +29,11 @@ public abstract class RelationView<D> {
                 this(representation, UUID.randomUUID().toString());
         }
 
-        public abstract int getArity();
-
         public Relation<D> getRepresentation() {
                 return representation;
         }
 
+        @Override
         public String getName() {
                 return representation.getName() + "#" + name;
         }