6 files changed, 388 insertions, 0 deletions

diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/AbstractRecursiveRewriter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/AbstractRecursiveRewriter.java
new file mode 100644
index 00000000..fb4c14a7
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/AbstractRecursiveRewriter.java
@@ -0,0 +1,26 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.rewriter;
+
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.equality.DnfEqualityChecker;
+import tools.refinery.store.util.CycleDetectingMapper;
+
+public abstract class AbstractRecursiveRewriter implements DnfRewriter {
+        private final CycleDetectingMapper<Dnf, Dnf> mapper = new CycleDetectingMapper<>(Dnf::name, this::map);
+
+        @Override
+        public Dnf rewrite(Dnf dnf) {
+                return mapper.map(dnf);
+        }
+
+        protected Dnf map(Dnf dnf) {
+                var result = doRewrite(dnf);
+                return dnf.equalsWithSubstitution(DnfEqualityChecker.DEFAULT, result) ? dnf : result;
+        }
+
+        protected abstract Dnf doRewrite(Dnf dnf);
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/ClauseInputParameterResolver.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/ClauseInputParameterResolver.java
new file mode 100644
index 00000000..aa06a05a
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/ClauseInputParameterResolver.java
@@ -0,0 +1,160 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.rewriter;
+
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.dnf.DnfClause;
+import tools.refinery.store.query.literal.*;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.ParameterDirection;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.*;
+
+class ClauseInputParameterResolver {
+        private final InputParameterResolver rewriter;
+        private final String dnfName;
+        private final int clauseIndex;
+        private final Set<Variable> positiveVariables = new LinkedHashSet<>();
+        private final List<Literal> inlinedLiterals = new ArrayList<>();
+        private final Deque<Literal> workList;
+        private int helperIndex = 0;
+
+        public ClauseInputParameterResolver(InputParameterResolver rewriter, List<Literal> context, DnfClause clause,
+                                                                                String dnfName, int clauseIndex) {
+                this.rewriter = rewriter;
+                this.dnfName = dnfName;
+                this.clauseIndex = clauseIndex;
+                workList = new ArrayDeque<>(clause.literals().size() + context.size());
+                for (var literal : context) {
+                        workList.addLast(literal);
+                }
+                for (var literal : clause.literals()) {
+                        workList.addLast(literal);
+                }
+        }
+
+        public List<Literal> rewriteClause() {
+                while (!workList.isEmpty()) {
+                        var literal = workList.removeFirst();
+                        processLiteral(literal);
+                }
+                return inlinedLiterals;
+        }
+
+        private void processLiteral(Literal literal) {
+                if (!(literal instanceof AbstractCallLiteral abstractCallLiteral) ||
+                                !(abstractCallLiteral.getTarget() instanceof Dnf targetDnf)) {
+                        markAsDone(literal);
+                        return;
+                }
+                boolean hasInputParameter = hasInputParameter(targetDnf);
+                if (!hasInputParameter) {
+                        targetDnf = rewriter.rewrite(targetDnf);
+                }
+                if (inlinePositiveClause(abstractCallLiteral, targetDnf)) {
+                        return;
+                }
+                if (eliminateDoubleNegation(abstractCallLiteral, targetDnf)) {
+                        return;
+                }
+                if (hasInputParameter) {
+                        rewriteWithCurrentContext(abstractCallLiteral, targetDnf);
+                        return;
+                }
+                markAsDone(abstractCallLiteral.withTarget(targetDnf));
+        }
+
+        private void markAsDone(Literal literal) {
+                positiveVariables.addAll(literal.getOutputVariables());
+                inlinedLiterals.add(literal);
+        }
+
+        private boolean inlinePositiveClause(AbstractCallLiteral abstractCallLiteral, Dnf targetDnf) {
+                var targetLiteral = getSingleLiteral(abstractCallLiteral, targetDnf, CallPolarity.POSITIVE);
+                if (targetLiteral == null) {
+                        return false;
+                }
+                var substitution = asSubstitution(abstractCallLiteral, targetDnf);
+                var substitutedLiteral = targetLiteral.substitute(substitution);
+                workList.addFirst(substitutedLiteral);
+                return true;
+        }
+
+        private boolean eliminateDoubleNegation(AbstractCallLiteral abstractCallLiteral, Dnf targetDnf) {
+                var targetLiteral = getSingleLiteral(abstractCallLiteral, targetDnf, CallPolarity.NEGATIVE);
+                if (!(targetLiteral instanceof CallLiteral targetCallLiteral) ||
+                                targetCallLiteral.getPolarity() != CallPolarity.NEGATIVE) {
+                        return false;
+                }
+                var substitution = asSubstitution(abstractCallLiteral, targetDnf);
+                var substitutedLiteral = (CallLiteral) targetCallLiteral.substitute(substitution);
+                workList.addFirst(substitutedLiteral.negate());
+                return true;
+        }
+
+        private void rewriteWithCurrentContext(AbstractCallLiteral abstractCallLiteral, Dnf targetDnf) {
+                var contextBuilder = Dnf.builder("%s#clause%d#helper%d".formatted(dnfName, clauseIndex, helperIndex));
+                helperIndex++;
+                contextBuilder.parameters(positiveVariables, ParameterDirection.OUT);
+                contextBuilder.clause(inlinedLiterals);
+                var contextDnf = contextBuilder.build();
+                var contextCall = new CallLiteral(CallPolarity.POSITIVE, contextDnf, List.copyOf(positiveVariables));
+                inlinedLiterals.clear();
+                var substitution = Substitution.builder().renewing().build();
+                var context = new ArrayList<Literal>();
+                context.add(contextCall.substitute(substitution));
+                int arity = targetDnf.arity();
+                for (int i = 0; i < arity; i++) {
+                        var parameter = targetDnf.getSymbolicParameters().get(i).getVariable();
+                        var argument = abstractCallLiteral.getArguments().get(i);
+                        context.add(new EquivalenceLiteral(true, parameter, substitution.getSubstitute(argument)));
+                }
+                var rewrittenDnf = rewriter.rewriteWithContext(context, targetDnf);
+                workList.addFirst(abstractCallLiteral.withTarget(rewrittenDnf));
+                workList.addFirst(contextCall);
+        }
+
+        private static boolean hasInputParameter(Dnf targetDnf) {
+                for (var parameter : targetDnf.getParameters()) {
+                        if (parameter.getDirection() != ParameterDirection.OUT) {
+                                return true;
+                        }
+                }
+                return false;
+        }
+
+        private static Literal getSingleLiteral(AbstractCallLiteral abstractCallLiteral, Dnf targetDnf,
+                                                                                        CallPolarity polarity) {
+                if (!(abstractCallLiteral instanceof CallLiteral callLiteral) ||
+                                callLiteral.getPolarity() != polarity) {
+                        return null;
+                }
+                var clauses = targetDnf.getClauses();
+                if (clauses.size() != 1) {
+                        return null;
+                }
+                var targetLiterals = clauses.get(0).literals();
+                if (targetLiterals.size() != 1) {
+                        return null;
+                }
+                return targetLiterals.get(0);
+        }
+
+        private static Substitution asSubstitution(AbstractCallLiteral callLiteral, Dnf targetDnf) {
+                var builder = Substitution.builder().renewing();
+                var arguments = callLiteral.getArguments();
+                var parameters = targetDnf.getSymbolicParameters();
+                int arity = arguments.size();
+                if (parameters.size() != arity) {
+                        throw new IllegalArgumentException("Call %s of %s arity mismatch".formatted(callLiteral, targetDnf));
+                }
+                for (int i = 0; i < arity; i++) {
+                        builder.putChecked(parameters.get(i).getVariable(), arguments.get(i));
+                }
+                return builder.build();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/CompositeRewriter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/CompositeRewriter.java
new file mode 100644
index 00000000..5b4f65e5
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/CompositeRewriter.java
@@ -0,0 +1,29 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.rewriter;
+
+import tools.refinery.store.query.dnf.Dnf;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class CompositeRewriter implements DnfRewriter {
+        private final List<DnfRewriter> rewriterList = new ArrayList<>();
+
+        public void addFirst(DnfRewriter rewriter) {
+                rewriterList.add(rewriter);
+        }
+
+        @Override
+        public Dnf rewrite(Dnf dnf) {
+                Dnf rewrittenDnf = dnf;
+                for (int i = rewriterList.size() - 1; i >= 0; i--) {
+                        var rewriter = rewriterList.get(i);
+                        rewrittenDnf = rewriter.rewrite(rewrittenDnf);
+                }
+                return rewrittenDnf;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/DnfRewriter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/DnfRewriter.java
new file mode 100644
index 00000000..5d8359d1
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/DnfRewriter.java
@@ -0,0 +1,24 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.rewriter;
+
+import tools.refinery.store.query.dnf.AnyQuery;
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.dnf.Query;
+
+@FunctionalInterface
+public interface DnfRewriter {
+        Dnf rewrite(Dnf dnf);
+
+        default AnyQuery rewrite(AnyQuery query) {
+                return rewrite((Query<?>) query);
+        }
+
+        default <T> Query<T> rewrite(Query<T> query) {
+                var rewrittenDnf = rewrite(query.getDnf());
+                return query.withDnf(rewrittenDnf);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/DuplicateDnfRemover.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/DuplicateDnfRemover.java
new file mode 100644
index 00000000..0c786470
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/DuplicateDnfRemover.java
@@ -0,0 +1,98 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.rewriter;
+
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.dnf.DnfClause;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.equality.DnfEqualityChecker;
+import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.Literal;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+public class DuplicateDnfRemover extends AbstractRecursiveRewriter {
+        private final Map<CanonicalDnf, Dnf> dnfCache = new HashMap<>();
+        private final Map<Dnf, Query<?>> queryCache = new HashMap<>();
+
+        @Override
+        protected Dnf map(Dnf dnf) {
+                var result = super.map(dnf);
+                return dnfCache.computeIfAbsent(new CanonicalDnf(result), CanonicalDnf::getDnf);
+        }
+
+        @Override
+        protected Dnf doRewrite(Dnf dnf) {
+                var builder = Dnf.builderFrom(dnf);
+                for (var clause : dnf.getClauses()) {
+                        builder.clause(rewriteClause(clause));
+                }
+                return builder.build();
+        }
+
+        private List<Literal> rewriteClause(DnfClause clause) {
+                var originalLiterals = clause.literals();
+                var literals = new ArrayList<Literal>(originalLiterals.size());
+                for (var literal : originalLiterals) {
+                        var rewrittenLiteral = literal;
+                        if (literal instanceof AbstractCallLiteral abstractCallLiteral &&
+                                        abstractCallLiteral.getTarget() instanceof Dnf targetDnf) {
+                                var rewrittenTarget = rewrite(targetDnf);
+                                rewrittenLiteral = abstractCallLiteral.withTarget(rewrittenTarget);
+                        }
+                        literals.add(rewrittenLiteral);
+                }
+                return literals;
+        }
+
+        @Override
+        public <T> Query<T> rewrite(Query<T> query) {
+                var rewrittenDnf = rewrite(query.getDnf());
+                // {@code withDnf} will always return the appropriate type.
+                @SuppressWarnings("unchecked")
+                var rewrittenQuery = (Query<T>) queryCache.computeIfAbsent(rewrittenDnf, query::withDnf);
+                return rewrittenQuery;
+        }
+
+        private static class CanonicalDnf {
+                private final Dnf dnf;
+                private final int hash;
+
+                public CanonicalDnf(Dnf dnf) {
+                        this.dnf = dnf;
+                        hash = dnf.hashCodeWithSubstitution();
+                }
+
+                public Dnf getDnf() {
+                        return dnf;
+                }
+
+                @Override
+                public boolean equals(Object obj) {
+                        if (this == obj) {
+                                return true;
+                        }
+                        if (obj == null || getClass() != obj.getClass()) {
+                                return false;
+                        }
+                        var otherCanonicalDnf = (CanonicalDnf) obj;
+                        return dnf.equalsWithSubstitution(DnfEqualityChecker.DEFAULT, otherCanonicalDnf.dnf);
+                }
+
+                @Override
+                public int hashCode() {
+                        return hash;
+                }
+
+                @Override
+                public String toString() {
+                        return dnf.name();
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/InputParameterResolver.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/InputParameterResolver.java
new file mode 100644
index 00000000..cd8a2e7d
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/rewriter/InputParameterResolver.java
@@ -0,0 +1,51 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.rewriter;
+
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.dnf.DnfBuilder;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.term.ParameterDirection;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.HashSet;
+import java.util.List;
+
+public class InputParameterResolver extends AbstractRecursiveRewriter {
+        @Override
+        protected Dnf doRewrite(Dnf dnf) {
+                return rewriteWithContext(List.of(), dnf);
+        }
+
+        Dnf rewriteWithContext(List<Literal> context, Dnf dnf) {
+                var dnfName = dnf.name();
+                var builder = Dnf.builder(dnfName);
+                createSymbolicParameters(context, dnf, builder);
+                builder.functionalDependencies(dnf.getFunctionalDependencies());
+                var clauses = dnf.getClauses();
+                int clauseCount = clauses.size();
+                for (int i = 0; i < clauseCount; i++) {
+                        var clause = clauses.get(i);
+                        var clauseRewriter = new ClauseInputParameterResolver(this, context, clause, dnfName, i);
+                        builder.clause(clauseRewriter.rewriteClause());
+                }
+                return builder.build();
+        }
+
+        private static void createSymbolicParameters(List<Literal> context, Dnf dnf, DnfBuilder builder) {
+                var positiveInContext = new HashSet<Variable>();
+                for (var literal : context) {
+                        positiveInContext.addAll(literal.getOutputVariables());
+                }
+                for (var symbolicParameter : dnf.getSymbolicParameters()) {
+                        var variable = symbolicParameter.getVariable();
+                        var isOutput = symbolicParameter.getDirection() == ParameterDirection.OUT ||
+                                        positiveInContext.contains(variable);
+                        var direction = isOutput ? ParameterDirection.OUT : ParameterDirection.IN;
+                        builder.parameter(variable, direction);
+                }
+        }
+}