From f3e42e7a09140fb68af534aca3e8df02c6c46ec7 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 1 May 2023 23:53:01 +0200 Subject: feat: count and aggregation literal reduction --- .../tools/refinery/store/query/Constraint.java | 4 +- .../java/tools/refinery/store/query/Reduction.java | 31 +++++ .../store/query/dnf/ClausePostProcessor.java | 24 ++-- .../java/tools/refinery/store/query/dnf/Dnf.java | 10 +- .../store/query/literal/AggregationLiteral.java | 29 +++-- .../store/query/literal/AssignLiteral.java | 8 +- .../store/query/literal/AssumeLiteral.java | 18 +-- .../store/query/literal/BooleanLiteral.java | 9 +- .../refinery/store/query/literal/CallLiteral.java | 17 ++- .../store/query/literal/ConstantLiteral.java | 8 +- .../refinery/store/query/literal/CountLiteral.java | 21 +++- .../store/query/literal/EquivalenceLiteral.java | 14 +-- .../refinery/store/query/literal/Literal.java | 6 +- .../store/query/literal/LiteralReduction.java | 31 ----- .../store/query/literal/VariableBinder.java | 64 ---------- .../store/query/literal/VariableBinderBuilder.java | 96 --------------- .../store/query/literal/VariableBindingSite.java | 64 ++++++++++ .../query/literal/VariableBindingSiteBuilder.java | 137 +++++++++++++++++++++ .../store/query/literal/VariableDirection.java | 85 +++++-------- .../tools/refinery/store/query/term/Parameter.java | 6 +- .../store/reasoning/literal/ModalConstraint.java | 4 +- 21 files changed, 367 insertions(+), 319 deletions(-) create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/Reduction.java delete mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java delete mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java delete mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSite.java create mode 100644 subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSiteBuilder.java (limited to 'subprojects') diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java index 207c627c..e841da9e 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java @@ -24,8 +24,8 @@ public interface Constraint { return i < 0 || i >= arity(); } - default LiteralReduction getReduction() { - return LiteralReduction.NOT_REDUCIBLE; + default Reduction getReduction() { + return Reduction.NOT_REDUCIBLE; } default boolean equals(LiteralEqualityHelper helper, Constraint other) { diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Reduction.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Reduction.java new file mode 100644 index 00000000..82c52b04 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Reduction.java @@ -0,0 +1,31 @@ +/* + * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.query; + +public enum Reduction { + /** + * Signifies that a literal should be preserved in the clause. + */ + NOT_REDUCIBLE, + + /** + * Signifies that the literal may be omitted from the cause (if the model being queried is nonempty). + */ + ALWAYS_TRUE, + + /** + * Signifies that the clause with the literal may be omitted entirely. + */ + ALWAYS_FALSE; + + public Reduction negate() { + return switch (this) { + case NOT_REDUCIBLE -> NOT_REDUCIBLE; + case ALWAYS_TRUE -> ALWAYS_FALSE; + case ALWAYS_FALSE -> ALWAYS_TRUE; + }; + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java index 72bc06a1..467b8d52 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java @@ -6,6 +6,7 @@ package tools.refinery.store.query.dnf; import org.jetbrains.annotations.NotNull; +import tools.refinery.store.query.literal.BooleanLiteral; import tools.refinery.store.query.literal.EquivalenceLiteral; import tools.refinery.store.query.literal.Literal; import tools.refinery.store.query.literal.VariableDirection; @@ -51,18 +52,11 @@ class ClausePostProcessor { topologicallySortLiterals(); var filteredLiterals = new ArrayList(topologicallySortedLiterals.size()); for (var literal : topologicallySortedLiterals) { - var reduction = literal.getReduction(); - switch (reduction) { - case NOT_REDUCIBLE -> filteredLiterals.add(literal); - case ALWAYS_TRUE -> { - // Literals reducible to {@code true} can be omitted, because the model is always assumed to have at - // least on object. - } - case ALWAYS_FALSE -> { - // Clauses with {@code false} literals can be omitted entirely. + var reducedLiteral = literal.reduce(); + if (BooleanLiteral.FALSE.equals(reducedLiteral)) { return ConstantResult.ALWAYS_FALSE; - } - default -> throw new IllegalArgumentException("Invalid reduction: " + reduction); + } else if (!BooleanLiteral.TRUE.equals(reducedLiteral)) { + filteredLiterals.add(reducedLiteral); } } if (filteredLiterals.isEmpty()) { @@ -156,7 +150,7 @@ class ClausePostProcessor { private void computePositiveVariables() { for (var literal : substitutedLiterals) { - var variableBinder = literal.getVariableBinder(); + var variableBinder = literal.getVariableBindingSite(); variableBinder.getVariablesWithDirection(VariableDirection.IN_OUT) .forEach(existentiallyQuantifiedVariables::add); variableBinder.getVariablesWithDirection(VariableDirection.OUT).forEach(variable -> { @@ -192,7 +186,7 @@ class ClausePostProcessor { private void validateClosureVariables() { var negativeVariablesMap = new HashMap(); for (var literal : substitutedLiterals) { - var variableBinder = literal.getVariableBinder(); + var variableBinder = literal.getVariableBindingSite(); variableBinder.getVariablesWithDirection(VariableDirection.CLOSURE, positiveVariables) .forEach(variable -> { var oldLiteral = negativeVariablesMap.put(variable, literal); @@ -243,7 +237,7 @@ class ClausePostProcessor { private SortableLiteral(int index, Literal literal) { this.index = index; this.literal = literal; - remainingInputs = literal.getVariableBinder() + remainingInputs = literal.getVariableBindingSite() .getVariablesWithDirection(VariableDirection.IN, positiveVariables) .collect(Collectors.toCollection(HashSet::new)); remainingInputs.removeAll(inputParameters); @@ -288,7 +282,7 @@ class ClausePostProcessor { } // Add literal if we haven't yet added a duplicate of this literal. topologicallySortedLiterals.add(literal); - var variableBinder = literal.getVariableBinder(); + var variableBinder = literal.getVariableBindingSite(); variableBinder.getVariablesWithDirection(VariableDirection.IN_OUT) .forEach(ClausePostProcessor.this::topologicallySortVariable); variableBinder.getVariablesWithDirection(VariableDirection.OUT) diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java index 7e68d4a0..64790f42 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java @@ -6,9 +6,9 @@ package tools.refinery.store.query.dnf; import tools.refinery.store.query.Constraint; +import tools.refinery.store.query.Reduction; import tools.refinery.store.query.equality.DnfEqualityChecker; import tools.refinery.store.query.equality.LiteralEqualityHelper; -import tools.refinery.store.query.literal.LiteralReduction; import tools.refinery.store.query.term.Parameter; import tools.refinery.store.query.term.Variable; @@ -103,16 +103,16 @@ public final class Dnf implements Constraint { } @Override - public LiteralReduction getReduction() { + public Reduction getReduction() { if (clauses.isEmpty()) { - return LiteralReduction.ALWAYS_FALSE; + return Reduction.ALWAYS_FALSE; } for (var clause : clauses) { if (clause.literals().isEmpty()) { - return LiteralReduction.ALWAYS_TRUE; + return Reduction.ALWAYS_TRUE; } } - return LiteralReduction.NOT_REDUCIBLE; + return Reduction.NOT_REDUCIBLE; } public boolean equalsWithSubstitution(DnfEqualityChecker callEqualityChecker, Dnf other) { diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java index 2aa0a0d5..51a33c1f 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java @@ -9,6 +9,7 @@ import tools.refinery.store.query.Constraint; import tools.refinery.store.query.equality.LiteralEqualityHelper; import tools.refinery.store.query.substitution.Substitution; import tools.refinery.store.query.term.Aggregator; +import tools.refinery.store.query.term.ConstantTerm; import tools.refinery.store.query.term.DataVariable; import tools.refinery.store.query.term.Variable; @@ -19,7 +20,7 @@ public class AggregationLiteral extends AbstractCallLiteral { private final DataVariable resultVariable; private final DataVariable inputVariable; private final Aggregator aggregator; - private final VariableBinder variableBinder; + private final VariableBindingSite variableBindingSite; public AggregationLiteral(DataVariable resultVariable, Aggregator aggregator, DataVariable inputVariable, Constraint target, List arguments) { @@ -39,13 +40,13 @@ public class AggregationLiteral extends AbstractCallLiteral { this.resultVariable = resultVariable; this.inputVariable = inputVariable; this.aggregator = aggregator; - variableBinder = VariableBinder.builder() + variableBindingSite = VariableBindingSite.builder() .variable(resultVariable, VariableDirection.OUT) .parameterList(false, target.getParameters(), arguments) .build(); - if (variableBinder.getDirection(inputVariable) != VariableDirection.CLOSURE) { - throw new IllegalArgumentException("Input variable %s must appear in the argument list".formatted( - inputVariable)); + if (variableBindingSite.getDirection(inputVariable) != VariableDirection.CLOSURE) { + throw new IllegalArgumentException(("Input variable %s must appear in the argument list as an output " + + "variable and should not be bound anywhere else").formatted(inputVariable)); } } @@ -62,8 +63,22 @@ public class AggregationLiteral extends AbstractCallLiteral { } @Override - public VariableBinder getVariableBinder() { - return variableBinder; + public VariableBindingSite getVariableBindingSite() { + return variableBindingSite; + } + + @Override + public Literal reduce() { + var reduction = getTarget().getReduction(); + return switch (reduction) { + case ALWAYS_FALSE -> { + var emptyValue = aggregator.getEmptyResult(); + yield emptyValue == null ? BooleanLiteral.FALSE : + resultVariable.assign(new ConstantTerm<>(resultVariable.getType(), emptyValue)); + } + case ALWAYS_TRUE -> throw new IllegalArgumentException("Trying to aggregate over an infinite set"); + case NOT_REDUCIBLE -> this; + }; } @Override diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java index 4da92b90..079ba6bb 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java @@ -15,7 +15,7 @@ import java.util.Objects; public final class AssignLiteral implements Literal { private final DataVariable variable; private final Term term; - private final VariableBinder variableBinder; + private final VariableBindingSite variableBindingSite; public AssignLiteral(DataVariable variable, Term term) { if (!term.getType().equals(variable.getType())) { @@ -29,7 +29,7 @@ public final class AssignLiteral implements Literal { throw new IllegalArgumentException("Result variable %s must not appear in the term %s".formatted( variable, term)); } - variableBinder = VariableBinder.builder() + variableBindingSite = VariableBindingSite.builder() .variable(variable, VariableDirection.OUT) .variables(inputVariables, VariableDirection.IN) .build(); @@ -44,8 +44,8 @@ public final class AssignLiteral implements Literal { } @Override - public VariableBinder getVariableBinder() { - return variableBinder; + public VariableBindingSite getVariableBindingSite() { + return variableBindingSite; } @Override diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java index 61486e4c..3dfb8902 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java @@ -14,7 +14,7 @@ import java.util.Objects; public final class AssumeLiteral implements Literal { private final Term term; - private final VariableBinder variableBinder; + private final VariableBindingSite variableBindingSite; public AssumeLiteral(Term term) { if (!term.getType().equals(Boolean.class)) { @@ -22,7 +22,7 @@ public final class AssumeLiteral implements Literal { term, Boolean.class.getName(), term.getType().getName())); } this.term = term; - variableBinder = VariableBinder.builder() + variableBindingSite = VariableBindingSite.builder() .variables(term.getInputVariables(), VariableDirection.IN) .build(); } @@ -32,8 +32,8 @@ public final class AssumeLiteral implements Literal { } @Override - public VariableBinder getVariableBinder() { - return variableBinder; + public VariableBindingSite getVariableBindingSite() { + return variableBindingSite; } @Override @@ -51,13 +51,13 @@ public final class AssumeLiteral implements Literal { } @Override - public LiteralReduction getReduction() { + public Literal reduce() { if (term instanceof ConstantTerm constantTerm) { - // Return {@code ALWAYS_FALSE} for {@code false} or {@code null} literals. - return Boolean.TRUE.equals(constantTerm.getValue()) ? LiteralReduction.ALWAYS_TRUE : - LiteralReduction.ALWAYS_FALSE; + // Return {@link BooleanLiteral#FALSE} for {@code false} or {@code null} literals. + return Boolean.TRUE.equals(constantTerm.getValue()) ? BooleanLiteral.TRUE : + BooleanLiteral.FALSE; } - return LiteralReduction.NOT_REDUCIBLE; + return this; } @Override diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java index e61f0535..736b3537 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java @@ -19,8 +19,8 @@ public enum BooleanLiteral implements CanNegate { } @Override - public VariableBinder getVariableBinder() { - return VariableBinder.EMPTY; + public VariableBindingSite getVariableBindingSite() { + return VariableBindingSite.EMPTY; } @Override @@ -29,11 +29,6 @@ public enum BooleanLiteral implements CanNegate { return this; } - @Override - public LiteralReduction getReduction() { - return value ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE; - } - @Override public BooleanLiteral negate() { return fromBoolean(!value); diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java index dc6098a8..4f755e95 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java @@ -15,7 +15,7 @@ import java.util.Objects; public final class CallLiteral extends AbstractCallLiteral implements CanNegate { private final CallPolarity polarity; - private final VariableBinder variableBinder; + private final VariableBindingSite variableBindingSite; public CallLiteral(CallPolarity polarity, Constraint target, List arguments) { super(target, arguments); @@ -30,7 +30,7 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate< } } this.polarity = polarity; - variableBinder = VariableBinder.builder() + variableBindingSite = VariableBindingSite.builder() .parameterList(polarity.isPositive(), parameters, arguments) .build(); } @@ -40,8 +40,8 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate< } @Override - public VariableBinder getVariableBinder() { - return variableBinder; + public VariableBindingSite getVariableBindingSite() { + return variableBindingSite; } @Override @@ -50,9 +50,14 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate< } @Override - public LiteralReduction getReduction() { + public Literal reduce() { var reduction = getTarget().getReduction(); - return polarity.isPositive() ? reduction : reduction.negate(); + var negatedReduction = polarity.isPositive() ? reduction : reduction.negate(); + return switch (negatedReduction) { + case ALWAYS_TRUE -> BooleanLiteral.TRUE; + case ALWAYS_FALSE -> BooleanLiteral.FALSE; + default -> this; + }; } @Override diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java index 7466cb1d..1bc14bab 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java @@ -14,12 +14,12 @@ import java.util.Objects; public final class ConstantLiteral implements Literal { private final NodeVariable variable; private final int nodeId; - private final VariableBinder variableBinder; + private final VariableBindingSite variableBindingSite; public ConstantLiteral(NodeVariable variable, int nodeId) { this.variable = variable; this.nodeId = nodeId; - variableBinder = VariableBinder.builder().variable(variable, VariableDirection.IN_OUT).build(); + variableBindingSite = VariableBindingSite.builder().variable(variable, VariableDirection.IN_OUT).build(); } public NodeVariable getVariable() { @@ -31,8 +31,8 @@ public final class ConstantLiteral implements Literal { } @Override - public VariableBinder getVariableBinder() { - return variableBinder; + public VariableBindingSite getVariableBindingSite() { + return variableBindingSite; } @Override diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java index a602d982..0a47aa66 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java @@ -10,13 +10,14 @@ import tools.refinery.store.query.equality.LiteralEqualityHelper; import tools.refinery.store.query.substitution.Substitution; import tools.refinery.store.query.term.DataVariable; import tools.refinery.store.query.term.Variable; +import tools.refinery.store.query.term.int_.IntTerms; import java.util.List; import java.util.Objects; public class CountLiteral extends AbstractCallLiteral { private final DataVariable resultVariable; - private final VariableBinder variableBinder; + private final VariableBindingSite variableBindingSite; public CountLiteral(DataVariable resultVariable, Constraint target, List arguments) { super(target, arguments); @@ -29,7 +30,7 @@ public class CountLiteral extends AbstractCallLiteral { .formatted(resultVariable)); } this.resultVariable = resultVariable; - variableBinder = VariableBinder.builder() + variableBindingSite = VariableBindingSite.builder() .variable(resultVariable, VariableDirection.OUT) .parameterList(false, target.getParameters(), arguments) .build(); @@ -40,8 +41,20 @@ public class CountLiteral extends AbstractCallLiteral { } @Override - public VariableBinder getVariableBinder() { - return variableBinder; + public VariableBindingSite getVariableBindingSite() { + return variableBindingSite; + } + + @Override + public Literal reduce() { + var reduction = getTarget().getReduction(); + return switch (reduction) { + case ALWAYS_FALSE -> getResultVariable().assign(IntTerms.constant(0)); + // The only way a constant {@code true} predicate can be called in a negative position is to have all of + // its arguments bound as input variables. Thus, there will only be a single match. + case ALWAYS_TRUE -> getResultVariable().assign(IntTerms.constant(1)); + case NOT_REDUCIBLE -> this; + }; } @Override diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java index 794cee0d..b36c0e40 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java @@ -16,13 +16,13 @@ public final class EquivalenceLiteral private final boolean positive; private final NodeVariable left; private final NodeVariable right; - private final VariableBinder variableBinder; + private final VariableBindingSite variableBindingSite; public EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right) { this.positive = positive; this.left = left; this.right = right; - variableBinder = VariableBinder.builder() + variableBindingSite = VariableBindingSite.builder() .variable(left, positive ? VariableDirection.IN_OUT : VariableDirection.IN) .variable(right, VariableDirection.IN) .build(); @@ -41,8 +41,8 @@ public final class EquivalenceLiteral } @Override - public VariableBinder getVariableBinder() { - return variableBinder; + public VariableBindingSite getVariableBindingSite() { + return variableBindingSite; } @Override @@ -57,11 +57,11 @@ public final class EquivalenceLiteral } @Override - public LiteralReduction getReduction() { + public Literal reduce() { if (left.equals(right)) { - return positive ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE; + return positive ? BooleanLiteral.TRUE : BooleanLiteral.FALSE; } - return LiteralReduction.NOT_REDUCIBLE; + return this; } @Override diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java index c3c111a4..10e4cffd 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java @@ -9,12 +9,12 @@ import tools.refinery.store.query.equality.LiteralEqualityHelper; import tools.refinery.store.query.substitution.Substitution; public interface Literal { - VariableBinder getVariableBinder(); + VariableBindingSite getVariableBindingSite(); Literal substitute(Substitution substitution); - default LiteralReduction getReduction() { - return LiteralReduction.NOT_REDUCIBLE; + default Literal reduce() { + return this; } @SuppressWarnings("BooleanMethodIsAlwaysInverted") diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java deleted file mode 100644 index 9d8352ea..00000000 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java +++ /dev/null @@ -1,31 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.query.literal; - -public enum LiteralReduction { - /** - * Signifies that a literal should be preserved in the clause. - */ - NOT_REDUCIBLE, - - /** - * Signifies that the literal may be omitted from the cause (if the model being queried is nonempty). - */ - ALWAYS_TRUE, - - /** - * Signifies that the clause with the literal may be omitted entirely. - */ - ALWAYS_FALSE; - - public LiteralReduction negate() { - return switch (this) { - case NOT_REDUCIBLE -> NOT_REDUCIBLE; - case ALWAYS_TRUE -> ALWAYS_FALSE; - case ALWAYS_FALSE -> ALWAYS_TRUE; - }; - } -} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java deleted file mode 100644 index 5f43d07d..00000000 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java +++ /dev/null @@ -1,64 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.query.literal; - -import tools.refinery.store.query.term.Variable; - -import java.util.Map; -import java.util.Set; -import java.util.stream.Stream; - -public final class VariableBinder { - public static final VariableBinder EMPTY = new VariableBinder(Map.of()); - - private final Map directionMap; - - VariableBinder(Map directionMap) { - this.directionMap = directionMap; - } - - public VariableDirection getDirection(Variable variable) { - var direction = directionMap.get(variable); - if (direction == null) { - throw new IllegalArgumentException("No such variable " + variable); - } - return direction; - } - - public VariableDirection getDirection(Variable variable, Set positiveVariables) { - var direction = getDirection(variable); - return disambiguateDirection(direction, variable, positiveVariables); - } - - public Stream getVariablesWithDirection(VariableDirection direction) { - return directionMap.entrySet().stream() - .filter(pair -> pair.getValue() == direction) - .map(Map.Entry::getKey); - } - - public Stream getVariablesWithDirection(VariableDirection direction, - Set positiveVariables) { - if (direction == VariableDirection.NEGATIVE) { - throw new IllegalArgumentException("Use #getVariablesWithDirection(VariableDirection) if disambiguation " + - "of VariableDirection#NEGATIVE variables according to the containing DnfClose is not desired"); - } - return directionMap.entrySet().stream() - .filter(pair -> disambiguateDirection(pair.getValue(), pair.getKey(), positiveVariables) == direction) - .map(Map.Entry::getKey); - } - - private VariableDirection disambiguateDirection(VariableDirection direction, Variable variable, - Set positiveVariables) { - if (direction != VariableDirection.NEGATIVE) { - return direction; - } - return positiveVariables.contains(variable) ? VariableDirection.IN : VariableDirection.CLOSURE; - } - - public static VariableBinderBuilder builder() { - return new VariableBinderBuilder(); - } -} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java deleted file mode 100644 index b0d47240..00000000 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java +++ /dev/null @@ -1,96 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.query.literal; - -import tools.refinery.store.query.exceptions.IncompatibleParameterDirectionException; -import tools.refinery.store.query.term.*; - -import java.util.*; - -public final class VariableBinderBuilder { - private final Map directionMap = new LinkedHashMap<>(); - private final Set uniqueVariables = new HashSet<>(); - - VariableBinderBuilder() { - } - - public VariableBinderBuilder variable(Variable variable, VariableDirection direction) { - return variable(variable, direction, direction == VariableDirection.OUT); - } - - private VariableBinderBuilder variable(Variable variable, VariableDirection direction, boolean markAsUnique) { - validateDirection(variable, direction); - boolean unique = shouldBeUnique(variable, markAsUnique); - directionMap.compute(variable, (ignored, oldValue) -> { - if (oldValue == null) { - return direction; - } - if (unique) { - throw new IllegalArgumentException("Duplicate binding for variable " + variable); - } - try { - return oldValue.merge(direction); - } catch (IncompatibleParameterDirectionException e) { - var message = "%s for variable %s".formatted(e.getMessage(), variable); - throw new IncompatibleParameterDirectionException(message, e); - } - }); - return this; - } - - private static void validateDirection(Variable variable, VariableDirection direction) { - if (variable instanceof AnyDataVariable) { - if (direction == VariableDirection.IN_OUT) { - throw new IllegalArgumentException("%s direction is not supported for data variable %s" - .formatted(direction, variable)); - } - } else if (variable instanceof NodeVariable) { - if (direction == VariableDirection.OUT) { - throw new IllegalArgumentException("%s direction is not supported for node variable %s" - .formatted(direction, variable)); - } - } else { - throw new IllegalArgumentException("Unknown variable " + variable); - } - } - - private boolean shouldBeUnique(Variable variable, boolean markAsUnique) { - if (markAsUnique) { - uniqueVariables.add(variable); - return true; - } else { - return uniqueVariables.contains(variable); - } - } - - public VariableBinderBuilder variables(Collection variables, VariableDirection direction) { - for (var variable : variables) { - variable(variable, direction); - } - return this; - } - - public VariableBinderBuilder parameterList(boolean positive, List parameters, - List arguments) { - int arity = parameters.size(); - if (arity != arguments.size()) { - throw new IllegalArgumentException("Got %d arguments for %d parameters" - .formatted(arguments.size(), arity)); - } - for (int i = 0; i < arity; i++) { - var argument = arguments.get(i); - var parameter = parameters.get(i); - var parameterDirection = parameter.getDirection(); - var direction = VariableDirection.from(positive, parameterDirection); - variable(argument, direction, parameterDirection == ParameterDirection.OUT); - } - return this; - } - - public VariableBinder build() { - return new VariableBinder(directionMap); - } -} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSite.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSite.java new file mode 100644 index 00000000..624af045 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSite.java @@ -0,0 +1,64 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.query.literal; + +import tools.refinery.store.query.term.Variable; + +import java.util.Map; +import java.util.Set; +import java.util.stream.Stream; + +public final class VariableBindingSite { + public static final VariableBindingSite EMPTY = new VariableBindingSite(Map.of()); + + private final Map directionMap; + + VariableBindingSite(Map directionMap) { + this.directionMap = directionMap; + } + + public VariableDirection getDirection(Variable variable) { + var direction = directionMap.get(variable); + if (direction == null) { + throw new IllegalArgumentException("No such variable " + variable); + } + return direction; + } + + public VariableDirection getDirection(Variable variable, Set positiveVariables) { + var direction = getDirection(variable); + return disambiguateDirection(direction, variable, positiveVariables); + } + + public Stream getVariablesWithDirection(VariableDirection direction) { + return directionMap.entrySet().stream() + .filter(pair -> pair.getValue() == direction) + .map(Map.Entry::getKey); + } + + public Stream getVariablesWithDirection(VariableDirection direction, + Set positiveVariables) { + if (direction == VariableDirection.NEUTRAL) { + throw new IllegalArgumentException("Use #getVariablesWithDirection(VariableDirection) if disambiguation " + + "of VariableDirection#NEUTRAL variables according to the containing DnfClose is not desired"); + } + return directionMap.entrySet().stream() + .filter(pair -> disambiguateDirection(pair.getValue(), pair.getKey(), positiveVariables) == direction) + .map(Map.Entry::getKey); + } + + private VariableDirection disambiguateDirection(VariableDirection direction, Variable variable, + Set positiveVariables) { + if (direction != VariableDirection.NEUTRAL) { + return direction; + } + return positiveVariables.contains(variable) ? VariableDirection.IN : VariableDirection.CLOSURE; + } + + public static VariableBindingSiteBuilder builder() { + return new VariableBindingSiteBuilder(); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSiteBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSiteBuilder.java new file mode 100644 index 00000000..873db1ec --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSiteBuilder.java @@ -0,0 +1,137 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.query.literal; + +import tools.refinery.store.query.exceptions.IncompatibleParameterDirectionException; +import tools.refinery.store.query.term.*; + +import java.util.*; + +public final class VariableBindingSiteBuilder { + private final Map directionMap = new LinkedHashMap<>(); + private final Set nonUnifiableVariables = new HashSet<>(); + + VariableBindingSiteBuilder() { + } + + public VariableBindingSiteBuilder variable(Variable variable, VariableDirection direction) { + return variable(variable, direction, direction == VariableDirection.OUT); + } + + public VariableBindingSiteBuilder variable(Variable variable, VariableDirection direction, boolean markAsUnique) { + validateUnique(direction, markAsUnique); + validateDirection(variable, direction); + boolean unique; + if (markAsUnique) { + nonUnifiableVariables.add(variable); + unique = true; + } else { + unique = nonUnifiableVariables.contains(variable); + } + directionMap.compute(variable, (ignored, oldValue) -> { + if (oldValue == null) { + return direction; + } + if (unique) { + throw new IllegalArgumentException("Duplicate binding for variable " + variable); + } + try { + return merge(oldValue, direction); + } catch (IncompatibleParameterDirectionException e) { + var message = "%s for variable %s".formatted(e.getMessage(), variable); + throw new IncompatibleParameterDirectionException(message, e); + } + }); + return this; + } + + private static void validateUnique(VariableDirection direction, boolean markAsUnique) { + if (direction == VariableDirection.OUT && !markAsUnique) { + throw new IllegalArgumentException("OUT binding must be marked as non-unifiable"); + } + if (markAsUnique && (direction != VariableDirection.OUT && direction != VariableDirection.CLOSURE)) { + throw new IllegalArgumentException("Only OUT or CLOSURE binding may be marked as non-unifiable"); + } + } + + private static void validateDirection(Variable variable, VariableDirection direction) { + if (variable instanceof AnyDataVariable) { + if (direction == VariableDirection.IN_OUT) { + throw new IllegalArgumentException("%s direction is not supported for data variable %s" + .formatted(direction, variable)); + } + } else if (variable instanceof NodeVariable) { + if (direction == VariableDirection.OUT) { + throw new IllegalArgumentException("%s direction is not supported for node variable %s" + .formatted(direction, variable)); + } + } else { + throw new IllegalArgumentException("Unknown variable " + variable); + } + } + + private static VariableDirection merge(VariableDirection left, VariableDirection right) { + return switch (left) { + case IN_OUT -> switch (right) { + case IN_OUT -> VariableDirection.IN_OUT; + case OUT -> VariableDirection.OUT; + case IN, NEUTRAL -> VariableDirection.IN; + case CLOSURE -> throw incompatibleDirections(left, right); + }; + case OUT -> switch (right) { + case IN_OUT, OUT -> VariableDirection.OUT; + case IN, NEUTRAL, CLOSURE -> throw incompatibleDirections(left, right); + }; + case IN -> switch (right) { + case IN_OUT, NEUTRAL, IN -> VariableDirection.IN; + case OUT, CLOSURE -> throw incompatibleDirections(left, right); + }; + case NEUTRAL -> switch (right) { + case IN_OUT, IN -> VariableDirection.IN; + case NEUTRAL -> VariableDirection.NEUTRAL; + case CLOSURE -> VariableDirection.CLOSURE; + case OUT -> throw incompatibleDirections(left, right); + }; + case CLOSURE -> switch (right) { + case NEUTRAL, CLOSURE -> VariableDirection.CLOSURE; + case IN_OUT, IN, OUT -> throw incompatibleDirections(left, right); + }; + }; + } + + private static RuntimeException incompatibleDirections(VariableDirection left, VariableDirection right) { + return new IncompatibleParameterDirectionException("Incompatible variable directions %s and %s" + .formatted(left, right)); + } + + public VariableBindingSiteBuilder variables(Collection variables, VariableDirection direction) { + for (var variable : variables) { + variable(variable, direction); + } + return this; + } + + public VariableBindingSiteBuilder parameterList(boolean positive, List parameters, + List arguments) { + int arity = parameters.size(); + if (arity != arguments.size()) { + throw new IllegalArgumentException("Got %d arguments for %d parameters" + .formatted(arguments.size(), arity)); + } + for (int i = 0; i < arity; i++) { + var argument = arguments.get(i); + var parameter = parameters.get(i); + var parameterDirection = parameter.getDirection(); + var direction = VariableDirection.from(positive, parameterDirection); + variable(argument, direction, parameterDirection == ParameterDirection.OUT); + } + return this; + } + + public VariableBindingSite build() { + return new VariableBindingSite(directionMap); + } +} diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java index 444dcbbf..0b7a2960 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java @@ -5,44 +5,63 @@ */ package tools.refinery.store.query.literal; -import tools.refinery.store.query.exceptions.IncompatibleParameterDirectionException; import tools.refinery.store.query.term.ParameterDirection; +/** + * Directions of the flow of a variable to ro from a clause. + *

+ * During the evaluation of a clause + *

    + *
  1. reads already bound {@code IN} variables,
    2. + *
  2. enumerates over all possible bindings of {@code CLOSURE} variables, and
    3. + *
  3. + * produces bindings for + *
      + *
    • {@code IN_OUT} variables that may already be bound in clause (if they already have a binding, + * the existing values are compared to the new binding by {@link Object#equals(Object)}), and
      • + *
    • {@code OUT} variables that must not be already bound in the clause (because comparison by + * equality wouldn't produce an appropriate join).
      • + *
    + *
    4. + *
+ * Variables marked as {@code NEUTRAL} may act as {@code IN} or {@code CLOSURE} depending on whether they have an + * existing binding that can be read. + */ public enum VariableDirection { /** * Binds a node variable or check equality with a node variable. *

- * This is the usual direction for positive constraints on nodes. A data variable may have multiple {@code InOut} + * This is the usual direction for positive constraints on nodes. A data variable may have multiple {@code IN_OUT} * bindings, even on the same parameter list. *

* Cannot be used for data variables. */ - IN_OUT("@InOut"), + IN_OUT, /** * Binds a data variable. *

- * A single variable must have at most one {@code @Out} binding. A variable with a {@code @Out} binding cannot + * A single variable must have at most one {@code OUT} binding. A variable with a {@code OUT} binding cannot * appear in any other place in a parameter list. *

* Cannot be used for node variables. */ - OUT("@Out"), + OUT, /** - * Either takes a bound data variable or enumerates all possible data variable bindings. + * Takes an already bound variable. *

- * Cannot be used for data variables. + * May be used with node or data variables. An {@code IN_OUT} or {@code OUT} binding on the same parameter list + * cannot satisfy the {@code IN} binding, because it might introduce a (non-monotonic) circular dependency. */ - NEGATIVE("@Negative"), + IN, /** - * Takes an already bound variable. + * Either takes a bound data variable or enumerates all possible data variable bindings. *

- * May be used with node or data variables. An {@code @InOut} or {@code @Out} binding on the same parameter list - * cannot satisfy the {@code @In} binding, because it might introduce a (non-monotonic) circular dependency. + * Cannot be used for data variables. */ - IN("@In"), + NEUTRAL, /** * Enumerates over all possible data variable bindings. @@ -51,49 +70,11 @@ public enum VariableDirection { * variable may only appear once in the parameter list, but node variables can appear multiple times to form * diagonal constraints. */ - CLOSURE("@Closure"); - - private final String name; - - VariableDirection(String name) { - this.name = name; - } - - public VariableDirection merge(VariableDirection other) { - switch (this) { - case IN_OUT -> { - if (other == IN_OUT) { - return this; - } - } - case OUT -> { - if (other == OUT) { - throw new IncompatibleParameterDirectionException("Multiple %s bindings".formatted(this)); - } - } - case NEGATIVE -> { - if (other == NEGATIVE || other == IN || other == CLOSURE) { - return other; - } - } - case IN, CLOSURE -> { - if (other == NEGATIVE || other == this) { - return this; - } - } - } - throw new IncompatibleParameterDirectionException("Incompatible variable directions %s and %s" - .formatted(this, other)); - } - - @Override - public String toString() { - return name; - } + CLOSURE; public static VariableDirection from(boolean positive, ParameterDirection parameterDirection) { return switch (parameterDirection) { - case IN_OUT -> positive ? IN_OUT : NEGATIVE; + case IN_OUT -> positive ? IN_OUT : NEUTRAL; case OUT -> positive ? OUT : CLOSURE; case IN -> IN; }; diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Parameter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Parameter.java index 29aedbef..351a353d 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Parameter.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Parameter.java @@ -26,8 +26,12 @@ public class Parameter { } } + public boolean isNodeVariable() { + return dataType == null; + } + public boolean isDataVariable() { - return dataType != null; + return !isNodeVariable(); } public Optional> tryGetType() { diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java index ce557d82..5ad1d5f8 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java @@ -7,7 +7,7 @@ package tools.refinery.store.reasoning.literal; import tools.refinery.store.query.Constraint; import tools.refinery.store.query.equality.LiteralEqualityHelper; -import tools.refinery.store.query.literal.LiteralReduction; +import tools.refinery.store.query.Reduction; import tools.refinery.store.query.term.Parameter; import java.util.List; @@ -26,7 +26,7 @@ public record ModalConstraint(Modality modality, Constraint constraint) implemen } @Override - public LiteralReduction getReduction() { + public Reduction getReduction() { return constraint.getReduction(); } -- cgit v1.2.3-54-g00ecf