diff options
19 files changed, 283 insertions, 235 deletions
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java index 207c627c..e841da9e 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java | |||
@@ -24,8 +24,8 @@ public interface Constraint { | |||
24 | return i < 0 || i >= arity(); | 24 | return i < 0 || i >= arity(); |
25 | } | 25 | } |
26 | 26 | ||
27 | default LiteralReduction getReduction() { | 27 | default Reduction getReduction() { |
28 | return LiteralReduction.NOT_REDUCIBLE; | 28 | return Reduction.NOT_REDUCIBLE; |
29 | } | 29 | } |
30 | 30 | ||
31 | default boolean equals(LiteralEqualityHelper helper, Constraint other) { | 31 | default boolean equals(LiteralEqualityHelper helper, Constraint other) { |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Reduction.java index 9d8352ea..82c52b04 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Reduction.java | |||
@@ -3,9 +3,9 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.query.literal; | 6 | package tools.refinery.store.query; |
7 | 7 | ||
8 | public enum LiteralReduction { | 8 | public enum Reduction { |
9 | /** | 9 | /** |
10 | * Signifies that a literal should be preserved in the clause. | 10 | * Signifies that a literal should be preserved in the clause. |
11 | */ | 11 | */ |
@@ -21,7 +21,7 @@ public enum LiteralReduction { | |||
21 | */ | 21 | */ |
22 | ALWAYS_FALSE; | 22 | ALWAYS_FALSE; |
23 | 23 | ||
24 | public LiteralReduction negate() { | 24 | public Reduction negate() { |
25 | return switch (this) { | 25 | return switch (this) { |
26 | case NOT_REDUCIBLE -> NOT_REDUCIBLE; | 26 | case NOT_REDUCIBLE -> NOT_REDUCIBLE; |
27 | case ALWAYS_TRUE -> ALWAYS_FALSE; | 27 | case ALWAYS_TRUE -> ALWAYS_FALSE; |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java index 72bc06a1..467b8d52 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java | |||
@@ -6,6 +6,7 @@ | |||
6 | package tools.refinery.store.query.dnf; | 6 | package tools.refinery.store.query.dnf; |
7 | 7 | ||
8 | import org.jetbrains.annotations.NotNull; | 8 | import org.jetbrains.annotations.NotNull; |
9 | import tools.refinery.store.query.literal.BooleanLiteral; | ||
9 | import tools.refinery.store.query.literal.EquivalenceLiteral; | 10 | import tools.refinery.store.query.literal.EquivalenceLiteral; |
10 | import tools.refinery.store.query.literal.Literal; | 11 | import tools.refinery.store.query.literal.Literal; |
11 | import tools.refinery.store.query.literal.VariableDirection; | 12 | import tools.refinery.store.query.literal.VariableDirection; |
@@ -51,18 +52,11 @@ class ClausePostProcessor { | |||
51 | topologicallySortLiterals(); | 52 | topologicallySortLiterals(); |
52 | var filteredLiterals = new ArrayList<Literal>(topologicallySortedLiterals.size()); | 53 | var filteredLiterals = new ArrayList<Literal>(topologicallySortedLiterals.size()); |
53 | for (var literal : topologicallySortedLiterals) { | 54 | for (var literal : topologicallySortedLiterals) { |
54 | var reduction = literal.getReduction(); | 55 | var reducedLiteral = literal.reduce(); |
55 | switch (reduction) { | 56 | if (BooleanLiteral.FALSE.equals(reducedLiteral)) { |
56 | case NOT_REDUCIBLE -> filteredLiterals.add(literal); | ||
57 | case ALWAYS_TRUE -> { | ||
58 | // Literals reducible to {@code true} can be omitted, because the model is always assumed to have at | ||
59 | // least on object. | ||
60 | } | ||
61 | case ALWAYS_FALSE -> { | ||
62 | // Clauses with {@code false} literals can be omitted entirely. | ||
63 | return ConstantResult.ALWAYS_FALSE; | 57 | return ConstantResult.ALWAYS_FALSE; |
64 | } | 58 | } else if (!BooleanLiteral.TRUE.equals(reducedLiteral)) { |
65 | default -> throw new IllegalArgumentException("Invalid reduction: " + reduction); | 59 | filteredLiterals.add(reducedLiteral); |
66 | } | 60 | } |
67 | } | 61 | } |
68 | if (filteredLiterals.isEmpty()) { | 62 | if (filteredLiterals.isEmpty()) { |
@@ -156,7 +150,7 @@ class ClausePostProcessor { | |||
156 | 150 | ||
157 | private void computePositiveVariables() { | 151 | private void computePositiveVariables() { |
158 | for (var literal : substitutedLiterals) { | 152 | for (var literal : substitutedLiterals) { |
159 | var variableBinder = literal.getVariableBinder(); | 153 | var variableBinder = literal.getVariableBindingSite(); |
160 | variableBinder.getVariablesWithDirection(VariableDirection.IN_OUT) | 154 | variableBinder.getVariablesWithDirection(VariableDirection.IN_OUT) |
161 | .forEach(existentiallyQuantifiedVariables::add); | 155 | .forEach(existentiallyQuantifiedVariables::add); |
162 | variableBinder.getVariablesWithDirection(VariableDirection.OUT).forEach(variable -> { | 156 | variableBinder.getVariablesWithDirection(VariableDirection.OUT).forEach(variable -> { |
@@ -192,7 +186,7 @@ class ClausePostProcessor { | |||
192 | private void validateClosureVariables() { | 186 | private void validateClosureVariables() { |
193 | var negativeVariablesMap = new HashMap<Variable, Literal>(); | 187 | var negativeVariablesMap = new HashMap<Variable, Literal>(); |
194 | for (var literal : substitutedLiterals) { | 188 | for (var literal : substitutedLiterals) { |
195 | var variableBinder = literal.getVariableBinder(); | 189 | var variableBinder = literal.getVariableBindingSite(); |
196 | variableBinder.getVariablesWithDirection(VariableDirection.CLOSURE, positiveVariables) | 190 | variableBinder.getVariablesWithDirection(VariableDirection.CLOSURE, positiveVariables) |
197 | .forEach(variable -> { | 191 | .forEach(variable -> { |
198 | var oldLiteral = negativeVariablesMap.put(variable, literal); | 192 | var oldLiteral = negativeVariablesMap.put(variable, literal); |
@@ -243,7 +237,7 @@ class ClausePostProcessor { | |||
243 | private SortableLiteral(int index, Literal literal) { | 237 | private SortableLiteral(int index, Literal literal) { |
244 | this.index = index; | 238 | this.index = index; |
245 | this.literal = literal; | 239 | this.literal = literal; |
246 | remainingInputs = literal.getVariableBinder() | 240 | remainingInputs = literal.getVariableBindingSite() |
247 | .getVariablesWithDirection(VariableDirection.IN, positiveVariables) | 241 | .getVariablesWithDirection(VariableDirection.IN, positiveVariables) |
248 | .collect(Collectors.toCollection(HashSet::new)); | 242 | .collect(Collectors.toCollection(HashSet::new)); |
249 | remainingInputs.removeAll(inputParameters); | 243 | remainingInputs.removeAll(inputParameters); |
@@ -288,7 +282,7 @@ class ClausePostProcessor { | |||
288 | } | 282 | } |
289 | // Add literal if we haven't yet added a duplicate of this literal. | 283 | // Add literal if we haven't yet added a duplicate of this literal. |
290 | topologicallySortedLiterals.add(literal); | 284 | topologicallySortedLiterals.add(literal); |
291 | var variableBinder = literal.getVariableBinder(); | 285 | var variableBinder = literal.getVariableBindingSite(); |
292 | variableBinder.getVariablesWithDirection(VariableDirection.IN_OUT) | 286 | variableBinder.getVariablesWithDirection(VariableDirection.IN_OUT) |
293 | .forEach(ClausePostProcessor.this::topologicallySortVariable); | 287 | .forEach(ClausePostProcessor.this::topologicallySortVariable); |
294 | variableBinder.getVariablesWithDirection(VariableDirection.OUT) | 288 | 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 @@ | |||
6 | package tools.refinery.store.query.dnf; | 6 | package tools.refinery.store.query.dnf; |
7 | 7 | ||
8 | import tools.refinery.store.query.Constraint; | 8 | import tools.refinery.store.query.Constraint; |
9 | import tools.refinery.store.query.Reduction; | ||
9 | import tools.refinery.store.query.equality.DnfEqualityChecker; | 10 | import tools.refinery.store.query.equality.DnfEqualityChecker; |
10 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | 11 | import tools.refinery.store.query.equality.LiteralEqualityHelper; |
11 | import tools.refinery.store.query.literal.LiteralReduction; | ||
12 | import tools.refinery.store.query.term.Parameter; | 12 | import tools.refinery.store.query.term.Parameter; |
13 | import tools.refinery.store.query.term.Variable; | 13 | import tools.refinery.store.query.term.Variable; |
14 | 14 | ||
@@ -103,16 +103,16 @@ public final class Dnf implements Constraint { | |||
103 | } | 103 | } |
104 | 104 | ||
105 | @Override | 105 | @Override |
106 | public LiteralReduction getReduction() { | 106 | public Reduction getReduction() { |
107 | if (clauses.isEmpty()) { | 107 | if (clauses.isEmpty()) { |
108 | return LiteralReduction.ALWAYS_FALSE; | 108 | return Reduction.ALWAYS_FALSE; |
109 | } | 109 | } |
110 | for (var clause : clauses) { | 110 | for (var clause : clauses) { |
111 | if (clause.literals().isEmpty()) { | 111 | if (clause.literals().isEmpty()) { |
112 | return LiteralReduction.ALWAYS_TRUE; | 112 | return Reduction.ALWAYS_TRUE; |
113 | } | 113 | } |
114 | } | 114 | } |
115 | return LiteralReduction.NOT_REDUCIBLE; | 115 | return Reduction.NOT_REDUCIBLE; |
116 | } | 116 | } |
117 | 117 | ||
118 | public boolean equalsWithSubstitution(DnfEqualityChecker callEqualityChecker, Dnf other) { | 118 | 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; | |||
9 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | 9 | import tools.refinery.store.query.equality.LiteralEqualityHelper; |
10 | import tools.refinery.store.query.substitution.Substitution; | 10 | import tools.refinery.store.query.substitution.Substitution; |
11 | import tools.refinery.store.query.term.Aggregator; | 11 | import tools.refinery.store.query.term.Aggregator; |
12 | import tools.refinery.store.query.term.ConstantTerm; | ||
12 | import tools.refinery.store.query.term.DataVariable; | 13 | import tools.refinery.store.query.term.DataVariable; |
13 | import tools.refinery.store.query.term.Variable; | 14 | import tools.refinery.store.query.term.Variable; |
14 | 15 | ||
@@ -19,7 +20,7 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral { | |||
19 | private final DataVariable<R> resultVariable; | 20 | private final DataVariable<R> resultVariable; |
20 | private final DataVariable<T> inputVariable; | 21 | private final DataVariable<T> inputVariable; |
21 | private final Aggregator<R, T> aggregator; | 22 | private final Aggregator<R, T> aggregator; |
22 | private final VariableBinder variableBinder; | 23 | private final VariableBindingSite variableBindingSite; |
23 | 24 | ||
24 | public AggregationLiteral(DataVariable<R> resultVariable, Aggregator<R, T> aggregator, | 25 | public AggregationLiteral(DataVariable<R> resultVariable, Aggregator<R, T> aggregator, |
25 | DataVariable<T> inputVariable, Constraint target, List<Variable> arguments) { | 26 | DataVariable<T> inputVariable, Constraint target, List<Variable> arguments) { |
@@ -39,13 +40,13 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral { | |||
39 | this.resultVariable = resultVariable; | 40 | this.resultVariable = resultVariable; |
40 | this.inputVariable = inputVariable; | 41 | this.inputVariable = inputVariable; |
41 | this.aggregator = aggregator; | 42 | this.aggregator = aggregator; |
42 | variableBinder = VariableBinder.builder() | 43 | variableBindingSite = VariableBindingSite.builder() |
43 | .variable(resultVariable, VariableDirection.OUT) | 44 | .variable(resultVariable, VariableDirection.OUT) |
44 | .parameterList(false, target.getParameters(), arguments) | 45 | .parameterList(false, target.getParameters(), arguments) |
45 | .build(); | 46 | .build(); |
46 | if (variableBinder.getDirection(inputVariable) != VariableDirection.CLOSURE) { | 47 | if (variableBindingSite.getDirection(inputVariable) != VariableDirection.CLOSURE) { |
47 | throw new IllegalArgumentException("Input variable %s must appear in the argument list".formatted( | 48 | throw new IllegalArgumentException(("Input variable %s must appear in the argument list as an output " + |
48 | inputVariable)); | 49 | "variable and should not be bound anywhere else").formatted(inputVariable)); |
49 | } | 50 | } |
50 | } | 51 | } |
51 | 52 | ||
@@ -62,8 +63,22 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral { | |||
62 | } | 63 | } |
63 | 64 | ||
64 | @Override | 65 | @Override |
65 | public VariableBinder getVariableBinder() { | 66 | public VariableBindingSite getVariableBindingSite() { |
66 | return variableBinder; | 67 | return variableBindingSite; |
68 | } | ||
69 | |||
70 | @Override | ||
71 | public Literal reduce() { | ||
72 | var reduction = getTarget().getReduction(); | ||
73 | return switch (reduction) { | ||
74 | case ALWAYS_FALSE -> { | ||
75 | var emptyValue = aggregator.getEmptyResult(); | ||
76 | yield emptyValue == null ? BooleanLiteral.FALSE : | ||
77 | resultVariable.assign(new ConstantTerm<>(resultVariable.getType(), emptyValue)); | ||
78 | } | ||
79 | case ALWAYS_TRUE -> throw new IllegalArgumentException("Trying to aggregate over an infinite set"); | ||
80 | case NOT_REDUCIBLE -> this; | ||
81 | }; | ||
67 | } | 82 | } |
68 | 83 | ||
69 | @Override | 84 | @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; | |||
15 | public final class AssignLiteral<T> implements Literal { | 15 | public final class AssignLiteral<T> implements Literal { |
16 | private final DataVariable<T> variable; | 16 | private final DataVariable<T> variable; |
17 | private final Term<T> term; | 17 | private final Term<T> term; |
18 | private final VariableBinder variableBinder; | 18 | private final VariableBindingSite variableBindingSite; |
19 | 19 | ||
20 | public AssignLiteral(DataVariable<T> variable, Term<T> term) { | 20 | public AssignLiteral(DataVariable<T> variable, Term<T> term) { |
21 | if (!term.getType().equals(variable.getType())) { | 21 | if (!term.getType().equals(variable.getType())) { |
@@ -29,7 +29,7 @@ public final class AssignLiteral<T> implements Literal { | |||
29 | throw new IllegalArgumentException("Result variable %s must not appear in the term %s".formatted( | 29 | throw new IllegalArgumentException("Result variable %s must not appear in the term %s".formatted( |
30 | variable, term)); | 30 | variable, term)); |
31 | } | 31 | } |
32 | variableBinder = VariableBinder.builder() | 32 | variableBindingSite = VariableBindingSite.builder() |
33 | .variable(variable, VariableDirection.OUT) | 33 | .variable(variable, VariableDirection.OUT) |
34 | .variables(inputVariables, VariableDirection.IN) | 34 | .variables(inputVariables, VariableDirection.IN) |
35 | .build(); | 35 | .build(); |
@@ -44,8 +44,8 @@ public final class AssignLiteral<T> implements Literal { | |||
44 | } | 44 | } |
45 | 45 | ||
46 | @Override | 46 | @Override |
47 | public VariableBinder getVariableBinder() { | 47 | public VariableBindingSite getVariableBindingSite() { |
48 | return variableBinder; | 48 | return variableBindingSite; |
49 | } | 49 | } |
50 | 50 | ||
51 | @Override | 51 | @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; | |||
14 | 14 | ||
15 | public final class AssumeLiteral implements Literal { | 15 | public final class AssumeLiteral implements Literal { |
16 | private final Term<Boolean> term; | 16 | private final Term<Boolean> term; |
17 | private final VariableBinder variableBinder; | 17 | private final VariableBindingSite variableBindingSite; |
18 | 18 | ||
19 | public AssumeLiteral(Term<Boolean> term) { | 19 | public AssumeLiteral(Term<Boolean> term) { |
20 | if (!term.getType().equals(Boolean.class)) { | 20 | if (!term.getType().equals(Boolean.class)) { |
@@ -22,7 +22,7 @@ public final class AssumeLiteral implements Literal { | |||
22 | term, Boolean.class.getName(), term.getType().getName())); | 22 | term, Boolean.class.getName(), term.getType().getName())); |
23 | } | 23 | } |
24 | this.term = term; | 24 | this.term = term; |
25 | variableBinder = VariableBinder.builder() | 25 | variableBindingSite = VariableBindingSite.builder() |
26 | .variables(term.getInputVariables(), VariableDirection.IN) | 26 | .variables(term.getInputVariables(), VariableDirection.IN) |
27 | .build(); | 27 | .build(); |
28 | } | 28 | } |
@@ -32,8 +32,8 @@ public final class AssumeLiteral implements Literal { | |||
32 | } | 32 | } |
33 | 33 | ||
34 | @Override | 34 | @Override |
35 | public VariableBinder getVariableBinder() { | 35 | public VariableBindingSite getVariableBindingSite() { |
36 | return variableBinder; | 36 | return variableBindingSite; |
37 | } | 37 | } |
38 | 38 | ||
39 | @Override | 39 | @Override |
@@ -51,13 +51,13 @@ public final class AssumeLiteral implements Literal { | |||
51 | } | 51 | } |
52 | 52 | ||
53 | @Override | 53 | @Override |
54 | public LiteralReduction getReduction() { | 54 | public Literal reduce() { |
55 | if (term instanceof ConstantTerm<Boolean> constantTerm) { | 55 | if (term instanceof ConstantTerm<Boolean> constantTerm) { |
56 | // Return {@code ALWAYS_FALSE} for {@code false} or {@code null} literals. | 56 | // Return {@link BooleanLiteral#FALSE} for {@code false} or {@code null} literals. |
57 | return Boolean.TRUE.equals(constantTerm.getValue()) ? LiteralReduction.ALWAYS_TRUE : | 57 | return Boolean.TRUE.equals(constantTerm.getValue()) ? BooleanLiteral.TRUE : |
58 | LiteralReduction.ALWAYS_FALSE; | 58 | BooleanLiteral.FALSE; |
59 | } | 59 | } |
60 | return LiteralReduction.NOT_REDUCIBLE; | 60 | return this; |
61 | } | 61 | } |
62 | 62 | ||
63 | @Override | 63 | @Override |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java index e61f0535..736b3537 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java | |||
@@ -19,8 +19,8 @@ public enum BooleanLiteral implements CanNegate<BooleanLiteral> { | |||
19 | } | 19 | } |
20 | 20 | ||
21 | @Override | 21 | @Override |
22 | public VariableBinder getVariableBinder() { | 22 | public VariableBindingSite getVariableBindingSite() { |
23 | return VariableBinder.EMPTY; | 23 | return VariableBindingSite.EMPTY; |
24 | } | 24 | } |
25 | 25 | ||
26 | @Override | 26 | @Override |
@@ -30,11 +30,6 @@ public enum BooleanLiteral implements CanNegate<BooleanLiteral> { | |||
30 | } | 30 | } |
31 | 31 | ||
32 | @Override | 32 | @Override |
33 | public LiteralReduction getReduction() { | ||
34 | return value ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE; | ||
35 | } | ||
36 | |||
37 | @Override | ||
38 | public BooleanLiteral negate() { | 33 | public BooleanLiteral negate() { |
39 | return fromBoolean(!value); | 34 | return fromBoolean(!value); |
40 | } | 35 | } |
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; | |||
15 | 15 | ||
16 | public final class CallLiteral extends AbstractCallLiteral implements CanNegate<CallLiteral> { | 16 | public final class CallLiteral extends AbstractCallLiteral implements CanNegate<CallLiteral> { |
17 | private final CallPolarity polarity; | 17 | private final CallPolarity polarity; |
18 | private final VariableBinder variableBinder; | 18 | private final VariableBindingSite variableBindingSite; |
19 | 19 | ||
20 | public CallLiteral(CallPolarity polarity, Constraint target, List<Variable> arguments) { | 20 | public CallLiteral(CallPolarity polarity, Constraint target, List<Variable> arguments) { |
21 | super(target, arguments); | 21 | super(target, arguments); |
@@ -30,7 +30,7 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate< | |||
30 | } | 30 | } |
31 | } | 31 | } |
32 | this.polarity = polarity; | 32 | this.polarity = polarity; |
33 | variableBinder = VariableBinder.builder() | 33 | variableBindingSite = VariableBindingSite.builder() |
34 | .parameterList(polarity.isPositive(), parameters, arguments) | 34 | .parameterList(polarity.isPositive(), parameters, arguments) |
35 | .build(); | 35 | .build(); |
36 | } | 36 | } |
@@ -40,8 +40,8 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate< | |||
40 | } | 40 | } |
41 | 41 | ||
42 | @Override | 42 | @Override |
43 | public VariableBinder getVariableBinder() { | 43 | public VariableBindingSite getVariableBindingSite() { |
44 | return variableBinder; | 44 | return variableBindingSite; |
45 | } | 45 | } |
46 | 46 | ||
47 | @Override | 47 | @Override |
@@ -50,9 +50,14 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate< | |||
50 | } | 50 | } |
51 | 51 | ||
52 | @Override | 52 | @Override |
53 | public LiteralReduction getReduction() { | 53 | public Literal reduce() { |
54 | var reduction = getTarget().getReduction(); | 54 | var reduction = getTarget().getReduction(); |
55 | return polarity.isPositive() ? reduction : reduction.negate(); | 55 | var negatedReduction = polarity.isPositive() ? reduction : reduction.negate(); |
56 | return switch (negatedReduction) { | ||
57 | case ALWAYS_TRUE -> BooleanLiteral.TRUE; | ||
58 | case ALWAYS_FALSE -> BooleanLiteral.FALSE; | ||
59 | default -> this; | ||
60 | }; | ||
56 | } | 61 | } |
57 | 62 | ||
58 | @Override | 63 | @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; | |||
14 | public final class ConstantLiteral implements Literal { | 14 | public final class ConstantLiteral implements Literal { |
15 | private final NodeVariable variable; | 15 | private final NodeVariable variable; |
16 | private final int nodeId; | 16 | private final int nodeId; |
17 | private final VariableBinder variableBinder; | 17 | private final VariableBindingSite variableBindingSite; |
18 | 18 | ||
19 | public ConstantLiteral(NodeVariable variable, int nodeId) { | 19 | public ConstantLiteral(NodeVariable variable, int nodeId) { |
20 | this.variable = variable; | 20 | this.variable = variable; |
21 | this.nodeId = nodeId; | 21 | this.nodeId = nodeId; |
22 | variableBinder = VariableBinder.builder().variable(variable, VariableDirection.IN_OUT).build(); | 22 | variableBindingSite = VariableBindingSite.builder().variable(variable, VariableDirection.IN_OUT).build(); |
23 | } | 23 | } |
24 | 24 | ||
25 | public NodeVariable getVariable() { | 25 | public NodeVariable getVariable() { |
@@ -31,8 +31,8 @@ public final class ConstantLiteral implements Literal { | |||
31 | } | 31 | } |
32 | 32 | ||
33 | @Override | 33 | @Override |
34 | public VariableBinder getVariableBinder() { | 34 | public VariableBindingSite getVariableBindingSite() { |
35 | return variableBinder; | 35 | return variableBindingSite; |
36 | } | 36 | } |
37 | 37 | ||
38 | @Override | 38 | @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; | |||
10 | import tools.refinery.store.query.substitution.Substitution; | 10 | import tools.refinery.store.query.substitution.Substitution; |
11 | import tools.refinery.store.query.term.DataVariable; | 11 | import tools.refinery.store.query.term.DataVariable; |
12 | import tools.refinery.store.query.term.Variable; | 12 | import tools.refinery.store.query.term.Variable; |
13 | import tools.refinery.store.query.term.int_.IntTerms; | ||
13 | 14 | ||
14 | import java.util.List; | 15 | import java.util.List; |
15 | import java.util.Objects; | 16 | import java.util.Objects; |
16 | 17 | ||
17 | public class CountLiteral extends AbstractCallLiteral { | 18 | public class CountLiteral extends AbstractCallLiteral { |
18 | private final DataVariable<Integer> resultVariable; | 19 | private final DataVariable<Integer> resultVariable; |
19 | private final VariableBinder variableBinder; | 20 | private final VariableBindingSite variableBindingSite; |
20 | 21 | ||
21 | public CountLiteral(DataVariable<Integer> resultVariable, Constraint target, List<Variable> arguments) { | 22 | public CountLiteral(DataVariable<Integer> resultVariable, Constraint target, List<Variable> arguments) { |
22 | super(target, arguments); | 23 | super(target, arguments); |
@@ -29,7 +30,7 @@ public class CountLiteral extends AbstractCallLiteral { | |||
29 | .formatted(resultVariable)); | 30 | .formatted(resultVariable)); |
30 | } | 31 | } |
31 | this.resultVariable = resultVariable; | 32 | this.resultVariable = resultVariable; |
32 | variableBinder = VariableBinder.builder() | 33 | variableBindingSite = VariableBindingSite.builder() |
33 | .variable(resultVariable, VariableDirection.OUT) | 34 | .variable(resultVariable, VariableDirection.OUT) |
34 | .parameterList(false, target.getParameters(), arguments) | 35 | .parameterList(false, target.getParameters(), arguments) |
35 | .build(); | 36 | .build(); |
@@ -40,8 +41,20 @@ public class CountLiteral extends AbstractCallLiteral { | |||
40 | } | 41 | } |
41 | 42 | ||
42 | @Override | 43 | @Override |
43 | public VariableBinder getVariableBinder() { | 44 | public VariableBindingSite getVariableBindingSite() { |
44 | return variableBinder; | 45 | return variableBindingSite; |
46 | } | ||
47 | |||
48 | @Override | ||
49 | public Literal reduce() { | ||
50 | var reduction = getTarget().getReduction(); | ||
51 | return switch (reduction) { | ||
52 | case ALWAYS_FALSE -> getResultVariable().assign(IntTerms.constant(0)); | ||
53 | // The only way a constant {@code true} predicate can be called in a negative position is to have all of | ||
54 | // its arguments bound as input variables. Thus, there will only be a single match. | ||
55 | case ALWAYS_TRUE -> getResultVariable().assign(IntTerms.constant(1)); | ||
56 | case NOT_REDUCIBLE -> this; | ||
57 | }; | ||
45 | } | 58 | } |
46 | 59 | ||
47 | @Override | 60 | @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 | |||
16 | private final boolean positive; | 16 | private final boolean positive; |
17 | private final NodeVariable left; | 17 | private final NodeVariable left; |
18 | private final NodeVariable right; | 18 | private final NodeVariable right; |
19 | private final VariableBinder variableBinder; | 19 | private final VariableBindingSite variableBindingSite; |
20 | 20 | ||
21 | public EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right) { | 21 | public EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right) { |
22 | this.positive = positive; | 22 | this.positive = positive; |
23 | this.left = left; | 23 | this.left = left; |
24 | this.right = right; | 24 | this.right = right; |
25 | variableBinder = VariableBinder.builder() | 25 | variableBindingSite = VariableBindingSite.builder() |
26 | .variable(left, positive ? VariableDirection.IN_OUT : VariableDirection.IN) | 26 | .variable(left, positive ? VariableDirection.IN_OUT : VariableDirection.IN) |
27 | .variable(right, VariableDirection.IN) | 27 | .variable(right, VariableDirection.IN) |
28 | .build(); | 28 | .build(); |
@@ -41,8 +41,8 @@ public final class EquivalenceLiteral | |||
41 | } | 41 | } |
42 | 42 | ||
43 | @Override | 43 | @Override |
44 | public VariableBinder getVariableBinder() { | 44 | public VariableBindingSite getVariableBindingSite() { |
45 | return variableBinder; | 45 | return variableBindingSite; |
46 | } | 46 | } |
47 | 47 | ||
48 | @Override | 48 | @Override |
@@ -57,11 +57,11 @@ public final class EquivalenceLiteral | |||
57 | } | 57 | } |
58 | 58 | ||
59 | @Override | 59 | @Override |
60 | public LiteralReduction getReduction() { | 60 | public Literal reduce() { |
61 | if (left.equals(right)) { | 61 | if (left.equals(right)) { |
62 | return positive ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE; | 62 | return positive ? BooleanLiteral.TRUE : BooleanLiteral.FALSE; |
63 | } | 63 | } |
64 | return LiteralReduction.NOT_REDUCIBLE; | 64 | return this; |
65 | } | 65 | } |
66 | 66 | ||
67 | @Override | 67 | @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; | |||
9 | import tools.refinery.store.query.substitution.Substitution; | 9 | import tools.refinery.store.query.substitution.Substitution; |
10 | 10 | ||
11 | public interface Literal { | 11 | public interface Literal { |
12 | VariableBinder getVariableBinder(); | 12 | VariableBindingSite getVariableBindingSite(); |
13 | 13 | ||
14 | Literal substitute(Substitution substitution); | 14 | Literal substitute(Substitution substitution); |
15 | 15 | ||
16 | default LiteralReduction getReduction() { | 16 | default Literal reduce() { |
17 | return LiteralReduction.NOT_REDUCIBLE; | 17 | return this; |
18 | } | 18 | } |
19 | 19 | ||
20 | @SuppressWarnings("BooleanMethodIsAlwaysInverted") | 20 | @SuppressWarnings("BooleanMethodIsAlwaysInverted") |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java deleted file mode 100644 index b0d47240..00000000 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java +++ /dev/null | |||
@@ -1,96 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.query.literal; | ||
7 | |||
8 | import tools.refinery.store.query.exceptions.IncompatibleParameterDirectionException; | ||
9 | import tools.refinery.store.query.term.*; | ||
10 | |||
11 | import java.util.*; | ||
12 | |||
13 | public final class VariableBinderBuilder { | ||
14 | private final Map<Variable, VariableDirection> directionMap = new LinkedHashMap<>(); | ||
15 | private final Set<Variable> uniqueVariables = new HashSet<>(); | ||
16 | |||
17 | VariableBinderBuilder() { | ||
18 | } | ||
19 | |||
20 | public VariableBinderBuilder variable(Variable variable, VariableDirection direction) { | ||
21 | return variable(variable, direction, direction == VariableDirection.OUT); | ||
22 | } | ||
23 | |||
24 | private VariableBinderBuilder variable(Variable variable, VariableDirection direction, boolean markAsUnique) { | ||
25 | validateDirection(variable, direction); | ||
26 | boolean unique = shouldBeUnique(variable, markAsUnique); | ||
27 | directionMap.compute(variable, (ignored, oldValue) -> { | ||
28 | if (oldValue == null) { | ||
29 | return direction; | ||
30 | } | ||
31 | if (unique) { | ||
32 | throw new IllegalArgumentException("Duplicate binding for variable " + variable); | ||
33 | } | ||
34 | try { | ||
35 | return oldValue.merge(direction); | ||
36 | } catch (IncompatibleParameterDirectionException e) { | ||
37 | var message = "%s for variable %s".formatted(e.getMessage(), variable); | ||
38 | throw new IncompatibleParameterDirectionException(message, e); | ||
39 | } | ||
40 | }); | ||
41 | return this; | ||
42 | } | ||
43 | |||
44 | private static void validateDirection(Variable variable, VariableDirection direction) { | ||
45 | if (variable instanceof AnyDataVariable) { | ||
46 | if (direction == VariableDirection.IN_OUT) { | ||
47 | throw new IllegalArgumentException("%s direction is not supported for data variable %s" | ||
48 | .formatted(direction, variable)); | ||
49 | } | ||
50 | } else if (variable instanceof NodeVariable) { | ||
51 | if (direction == VariableDirection.OUT) { | ||
52 | throw new IllegalArgumentException("%s direction is not supported for node variable %s" | ||
53 | .formatted(direction, variable)); | ||
54 | } | ||
55 | } else { | ||
56 | throw new IllegalArgumentException("Unknown variable " + variable); | ||
57 | } | ||
58 | } | ||
59 | |||
60 | private boolean shouldBeUnique(Variable variable, boolean markAsUnique) { | ||
61 | if (markAsUnique) { | ||
62 | uniqueVariables.add(variable); | ||
63 | return true; | ||
64 | } else { | ||
65 | return uniqueVariables.contains(variable); | ||
66 | } | ||
67 | } | ||
68 | |||
69 | public VariableBinderBuilder variables(Collection<? extends Variable> variables, VariableDirection direction) { | ||
70 | for (var variable : variables) { | ||
71 | variable(variable, direction); | ||
72 | } | ||
73 | return this; | ||
74 | } | ||
75 | |||
76 | public VariableBinderBuilder parameterList(boolean positive, List<Parameter> parameters, | ||
77 | List<Variable> arguments) { | ||
78 | int arity = parameters.size(); | ||
79 | if (arity != arguments.size()) { | ||
80 | throw new IllegalArgumentException("Got %d arguments for %d parameters" | ||
81 | .formatted(arguments.size(), arity)); | ||
82 | } | ||
83 | for (int i = 0; i < arity; i++) { | ||
84 | var argument = arguments.get(i); | ||
85 | var parameter = parameters.get(i); | ||
86 | var parameterDirection = parameter.getDirection(); | ||
87 | var direction = VariableDirection.from(positive, parameterDirection); | ||
88 | variable(argument, direction, parameterDirection == ParameterDirection.OUT); | ||
89 | } | ||
90 | return this; | ||
91 | } | ||
92 | |||
93 | public VariableBinder build() { | ||
94 | return new VariableBinder(directionMap); | ||
95 | } | ||
96 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSite.java index 5f43d07d..624af045 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBindingSite.java | |||
@@ -11,12 +11,12 @@ import java.util.Map; | |||
11 | import java.util.Set; | 11 | import java.util.Set; |
12 | import java.util.stream.Stream; | 12 | import java.util.stream.Stream; |
13 | 13 | ||
14 | public final class VariableBinder { | 14 | public final class VariableBindingSite { |
15 | public static final VariableBinder EMPTY = new VariableBinder(Map.of()); | 15 | public static final VariableBindingSite EMPTY = new VariableBindingSite(Map.of()); |
16 | 16 | ||
17 | private final Map<Variable, VariableDirection> directionMap; | 17 | private final Map<Variable, VariableDirection> directionMap; |
18 | 18 | ||
19 | VariableBinder(Map<Variable, VariableDirection> directionMap) { | 19 | VariableBindingSite(Map<Variable, VariableDirection> directionMap) { |
20 | this.directionMap = directionMap; | 20 | this.directionMap = directionMap; |
21 | } | 21 | } |
22 | 22 | ||
@@ -41,9 +41,9 @@ public final class VariableBinder { | |||
41 | 41 | ||
42 | public Stream<Variable> getVariablesWithDirection(VariableDirection direction, | 42 | public Stream<Variable> getVariablesWithDirection(VariableDirection direction, |
43 | Set<? extends Variable> positiveVariables) { | 43 | Set<? extends Variable> positiveVariables) { |
44 | if (direction == VariableDirection.NEGATIVE) { | 44 | if (direction == VariableDirection.NEUTRAL) { |
45 | throw new IllegalArgumentException("Use #getVariablesWithDirection(VariableDirection) if disambiguation " + | 45 | throw new IllegalArgumentException("Use #getVariablesWithDirection(VariableDirection) if disambiguation " + |
46 | "of VariableDirection#NEGATIVE variables according to the containing DnfClose is not desired"); | 46 | "of VariableDirection#NEUTRAL variables according to the containing DnfClose is not desired"); |
47 | } | 47 | } |
48 | return directionMap.entrySet().stream() | 48 | return directionMap.entrySet().stream() |
49 | .filter(pair -> disambiguateDirection(pair.getValue(), pair.getKey(), positiveVariables) == direction) | 49 | .filter(pair -> disambiguateDirection(pair.getValue(), pair.getKey(), positiveVariables) == direction) |
@@ -52,13 +52,13 @@ public final class VariableBinder { | |||
52 | 52 | ||
53 | private VariableDirection disambiguateDirection(VariableDirection direction, Variable variable, | 53 | private VariableDirection disambiguateDirection(VariableDirection direction, Variable variable, |
54 | Set<? extends Variable> positiveVariables) { | 54 | Set<? extends Variable> positiveVariables) { |
55 | if (direction != VariableDirection.NEGATIVE) { | 55 | if (direction != VariableDirection.NEUTRAL) { |
56 | return direction; | 56 | return direction; |
57 | } | 57 | } |
58 | return positiveVariables.contains(variable) ? VariableDirection.IN : VariableDirection.CLOSURE; | 58 | return positiveVariables.contains(variable) ? VariableDirection.IN : VariableDirection.CLOSURE; |
59 | } | 59 | } |
60 | 60 | ||
61 | public static VariableBinderBuilder builder() { | 61 | public static VariableBindingSiteBuilder builder() { |
62 | return new VariableBinderBuilder(); | 62 | return new VariableBindingSiteBuilder(); |
63 | } | 63 | } |
64 | } | 64 | } |
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 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.query.literal; | ||
7 | |||
8 | import tools.refinery.store.query.exceptions.IncompatibleParameterDirectionException; | ||
9 | import tools.refinery.store.query.term.*; | ||
10 | |||
11 | import java.util.*; | ||
12 | |||
13 | public final class VariableBindingSiteBuilder { | ||
14 | private final Map<Variable, VariableDirection> directionMap = new LinkedHashMap<>(); | ||
15 | private final Set<Variable> nonUnifiableVariables = new HashSet<>(); | ||
16 | |||
17 | VariableBindingSiteBuilder() { | ||
18 | } | ||
19 | |||
20 | public VariableBindingSiteBuilder variable(Variable variable, VariableDirection direction) { | ||
21 | return variable(variable, direction, direction == VariableDirection.OUT); | ||
22 | } | ||
23 | |||
24 | public VariableBindingSiteBuilder variable(Variable variable, VariableDirection direction, boolean markAsUnique) { | ||
25 | validateUnique(direction, markAsUnique); | ||
26 | validateDirection(variable, direction); | ||
27 | boolean unique; | ||
28 | if (markAsUnique) { | ||
29 | nonUnifiableVariables.add(variable); | ||
30 | unique = true; | ||
31 | } else { | ||
32 | unique = nonUnifiableVariables.contains(variable); | ||
33 | } | ||
34 | directionMap.compute(variable, (ignored, oldValue) -> { | ||
35 | if (oldValue == null) { | ||
36 | return direction; | ||
37 | } | ||
38 | if (unique) { | ||
39 | throw new IllegalArgumentException("Duplicate binding for variable " + variable); | ||
40 | } | ||
41 | try { | ||
42 | return merge(oldValue, direction); | ||
43 | } catch (IncompatibleParameterDirectionException e) { | ||
44 | var message = "%s for variable %s".formatted(e.getMessage(), variable); | ||
45 | throw new IncompatibleParameterDirectionException(message, e); | ||
46 | } | ||
47 | }); | ||
48 | return this; | ||
49 | } | ||
50 | |||
51 | private static void validateUnique(VariableDirection direction, boolean markAsUnique) { | ||
52 | if (direction == VariableDirection.OUT && !markAsUnique) { | ||
53 | throw new IllegalArgumentException("OUT binding must be marked as non-unifiable"); | ||
54 | } | ||
55 | if (markAsUnique && (direction != VariableDirection.OUT && direction != VariableDirection.CLOSURE)) { | ||
56 | throw new IllegalArgumentException("Only OUT or CLOSURE binding may be marked as non-unifiable"); | ||
57 | } | ||
58 | } | ||
59 | |||
60 | private static void validateDirection(Variable variable, VariableDirection direction) { | ||
61 | if (variable instanceof AnyDataVariable) { | ||
62 | if (direction == VariableDirection.IN_OUT) { | ||
63 | throw new IllegalArgumentException("%s direction is not supported for data variable %s" | ||
64 | .formatted(direction, variable)); | ||
65 | } | ||
66 | } else if (variable instanceof NodeVariable) { | ||
67 | if (direction == VariableDirection.OUT) { | ||
68 | throw new IllegalArgumentException("%s direction is not supported for node variable %s" | ||
69 | .formatted(direction, variable)); | ||
70 | } | ||
71 | } else { | ||
72 | throw new IllegalArgumentException("Unknown variable " + variable); | ||
73 | } | ||
74 | } | ||
75 | |||
76 | private static VariableDirection merge(VariableDirection left, VariableDirection right) { | ||
77 | return switch (left) { | ||
78 | case IN_OUT -> switch (right) { | ||
79 | case IN_OUT -> VariableDirection.IN_OUT; | ||
80 | case OUT -> VariableDirection.OUT; | ||
81 | case IN, NEUTRAL -> VariableDirection.IN; | ||
82 | case CLOSURE -> throw incompatibleDirections(left, right); | ||
83 | }; | ||
84 | case OUT -> switch (right) { | ||
85 | case IN_OUT, OUT -> VariableDirection.OUT; | ||
86 | case IN, NEUTRAL, CLOSURE -> throw incompatibleDirections(left, right); | ||
87 | }; | ||
88 | case IN -> switch (right) { | ||
89 | case IN_OUT, NEUTRAL, IN -> VariableDirection.IN; | ||
90 | case OUT, CLOSURE -> throw incompatibleDirections(left, right); | ||
91 | }; | ||
92 | case NEUTRAL -> switch (right) { | ||
93 | case IN_OUT, IN -> VariableDirection.IN; | ||
94 | case NEUTRAL -> VariableDirection.NEUTRAL; | ||
95 | case CLOSURE -> VariableDirection.CLOSURE; | ||
96 | case OUT -> throw incompatibleDirections(left, right); | ||
97 | }; | ||
98 | case CLOSURE -> switch (right) { | ||
99 | case NEUTRAL, CLOSURE -> VariableDirection.CLOSURE; | ||
100 | case IN_OUT, IN, OUT -> throw incompatibleDirections(left, right); | ||
101 | }; | ||
102 | }; | ||
103 | } | ||
104 | |||
105 | private static RuntimeException incompatibleDirections(VariableDirection left, VariableDirection right) { | ||
106 | return new IncompatibleParameterDirectionException("Incompatible variable directions %s and %s" | ||
107 | .formatted(left, right)); | ||
108 | } | ||
109 | |||
110 | public VariableBindingSiteBuilder variables(Collection<? extends Variable> variables, VariableDirection direction) { | ||
111 | for (var variable : variables) { | ||
112 | variable(variable, direction); | ||
113 | } | ||
114 | return this; | ||
115 | } | ||
116 | |||
117 | public VariableBindingSiteBuilder parameterList(boolean positive, List<Parameter> parameters, | ||
118 | List<Variable> arguments) { | ||
119 | int arity = parameters.size(); | ||
120 | if (arity != arguments.size()) { | ||
121 | throw new IllegalArgumentException("Got %d arguments for %d parameters" | ||
122 | .formatted(arguments.size(), arity)); | ||
123 | } | ||
124 | for (int i = 0; i < arity; i++) { | ||
125 | var argument = arguments.get(i); | ||
126 | var parameter = parameters.get(i); | ||
127 | var parameterDirection = parameter.getDirection(); | ||
128 | var direction = VariableDirection.from(positive, parameterDirection); | ||
129 | variable(argument, direction, parameterDirection == ParameterDirection.OUT); | ||
130 | } | ||
131 | return this; | ||
132 | } | ||
133 | |||
134 | public VariableBindingSite build() { | ||
135 | return new VariableBindingSite(directionMap); | ||
136 | } | ||
137 | } | ||
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 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.query.literal; | 6 | package tools.refinery.store.query.literal; |
7 | 7 | ||
8 | import tools.refinery.store.query.exceptions.IncompatibleParameterDirectionException; | ||
9 | import tools.refinery.store.query.term.ParameterDirection; | 8 | import tools.refinery.store.query.term.ParameterDirection; |
10 | 9 | ||
10 | /** | ||
11 | * Directions of the flow of a variable to ro from a clause. | ||
12 | * <p> | ||
13 | * During the evaluation of a clause | ||
14 | * <ol> | ||
15 | * <li>reads already bound {@code IN} variables,</li> | ||
16 | * <li>enumerates over all possible bindings of {@code CLOSURE} variables, and</li> | ||
17 | * <li> | ||
18 | * produces bindings for | ||
19 | * <ul> | ||
20 | * <li>{@code IN_OUT} variables that may already be bound in clause (if they already have a binding, | ||
21 | * the existing values are compared to the new binding by {@link Object#equals(Object)}), and</li> | ||
22 | * <li>{@code OUT} variables that must not be already bound in the clause (because comparison by | ||
23 | * equality wouldn't produce an appropriate join).</li> | ||
24 | * </ul> | ||
25 | * </li> | ||
26 | * </ol> | ||
27 | * Variables marked as {@code NEUTRAL} may act as {@code IN} or {@code CLOSURE} depending on whether they have an | ||
28 | * existing binding that can be read. | ||
29 | */ | ||
11 | public enum VariableDirection { | 30 | public enum VariableDirection { |
12 | /** | 31 | /** |
13 | * Binds a node variable or check equality with a node variable. | 32 | * Binds a node variable or check equality with a node variable. |
14 | * <p> | 33 | * <p> |
15 | * This is the usual direction for positive constraints on nodes. A data variable may have multiple {@code InOut} | 34 | * This is the usual direction for positive constraints on nodes. A data variable may have multiple {@code IN_OUT} |
16 | * bindings, even on the same parameter list. | 35 | * bindings, even on the same parameter list. |
17 | * <p> | 36 | * <p> |
18 | * Cannot be used for data variables. | 37 | * Cannot be used for data variables. |
19 | */ | 38 | */ |
20 | IN_OUT("@InOut"), | 39 | IN_OUT, |
21 | 40 | ||
22 | /** | 41 | /** |
23 | * Binds a data variable. | 42 | * Binds a data variable. |
24 | * <p> | 43 | * <p> |
25 | * A single variable must have at most one {@code @Out} binding. A variable with a {@code @Out} binding cannot | 44 | * A single variable must have at most one {@code OUT} binding. A variable with a {@code OUT} binding cannot |
26 | * appear in any other place in a parameter list. | 45 | * appear in any other place in a parameter list. |
27 | * <p> | 46 | * <p> |
28 | * Cannot be used for node variables. | 47 | * Cannot be used for node variables. |
29 | */ | 48 | */ |
30 | OUT("@Out"), | 49 | OUT, |
31 | 50 | ||
32 | /** | 51 | /** |
33 | * Either takes a bound data variable or enumerates all possible data variable bindings. | 52 | * Takes an already bound variable. |
34 | * <p> | 53 | * <p> |
35 | * Cannot be used for data variables. | 54 | * May be used with node or data variables. An {@code IN_OUT} or {@code OUT} binding on the same parameter list |
55 | * cannot satisfy the {@code IN} binding, because it might introduce a (non-monotonic) circular dependency. | ||
36 | */ | 56 | */ |
37 | NEGATIVE("@Negative"), | 57 | IN, |
38 | 58 | ||
39 | /** | 59 | /** |
40 | * Takes an already bound variable. | 60 | * Either takes a bound data variable or enumerates all possible data variable bindings. |
41 | * <p> | 61 | * <p> |
42 | * May be used with node or data variables. An {@code @InOut} or {@code @Out} binding on the same parameter list | 62 | * Cannot be used for data variables. |
43 | * cannot satisfy the {@code @In} binding, because it might introduce a (non-monotonic) circular dependency. | ||
44 | */ | 63 | */ |
45 | IN("@In"), | 64 | NEUTRAL, |
46 | 65 | ||
47 | /** | 66 | /** |
48 | * Enumerates over all possible data variable bindings. | 67 | * Enumerates over all possible data variable bindings. |
@@ -51,49 +70,11 @@ public enum VariableDirection { | |||
51 | * variable may only appear once in the parameter list, but node variables can appear multiple times to form | 70 | * variable may only appear once in the parameter list, but node variables can appear multiple times to form |
52 | * diagonal constraints. | 71 | * diagonal constraints. |
53 | */ | 72 | */ |
54 | CLOSURE("@Closure"); | 73 | CLOSURE; |
55 | |||
56 | private final String name; | ||
57 | |||
58 | VariableDirection(String name) { | ||
59 | this.name = name; | ||
60 | } | ||
61 | |||
62 | public VariableDirection merge(VariableDirection other) { | ||
63 | switch (this) { | ||
64 | case IN_OUT -> { | ||
65 | if (other == IN_OUT) { | ||
66 | return this; | ||
67 | } | ||
68 | } | ||
69 | case OUT -> { | ||
70 | if (other == OUT) { | ||
71 | throw new IncompatibleParameterDirectionException("Multiple %s bindings".formatted(this)); | ||
72 | } | ||
73 | } | ||
74 | case NEGATIVE -> { | ||
75 | if (other == NEGATIVE || other == IN || other == CLOSURE) { | ||
76 | return other; | ||
77 | } | ||
78 | } | ||
79 | case IN, CLOSURE -> { | ||
80 | if (other == NEGATIVE || other == this) { | ||
81 | return this; | ||
82 | } | ||
83 | } | ||
84 | } | ||
85 | throw new IncompatibleParameterDirectionException("Incompatible variable directions %s and %s" | ||
86 | .formatted(this, other)); | ||
87 | } | ||
88 | |||
89 | @Override | ||
90 | public String toString() { | ||
91 | return name; | ||
92 | } | ||
93 | 74 | ||
94 | public static VariableDirection from(boolean positive, ParameterDirection parameterDirection) { | 75 | public static VariableDirection from(boolean positive, ParameterDirection parameterDirection) { |
95 | return switch (parameterDirection) { | 76 | return switch (parameterDirection) { |
96 | case IN_OUT -> positive ? IN_OUT : NEGATIVE; | 77 | case IN_OUT -> positive ? IN_OUT : NEUTRAL; |
97 | case OUT -> positive ? OUT : CLOSURE; | 78 | case OUT -> positive ? OUT : CLOSURE; |
98 | case IN -> IN; | 79 | case IN -> IN; |
99 | }; | 80 | }; |
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 { | |||
26 | } | 26 | } |
27 | } | 27 | } |
28 | 28 | ||
29 | public boolean isNodeVariable() { | ||
30 | return dataType == null; | ||
31 | } | ||
32 | |||
29 | public boolean isDataVariable() { | 33 | public boolean isDataVariable() { |
30 | return dataType != null; | 34 | return !isNodeVariable(); |
31 | } | 35 | } |
32 | 36 | ||
33 | public Optional<Class<?>> tryGetType() { | 37 | public Optional<Class<?>> 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; | |||
7 | 7 | ||
8 | import tools.refinery.store.query.Constraint; | 8 | import tools.refinery.store.query.Constraint; |
9 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | 9 | import tools.refinery.store.query.equality.LiteralEqualityHelper; |
10 | import tools.refinery.store.query.literal.LiteralReduction; | 10 | import tools.refinery.store.query.Reduction; |
11 | import tools.refinery.store.query.term.Parameter; | 11 | import tools.refinery.store.query.term.Parameter; |
12 | 12 | ||
13 | import java.util.List; | 13 | import java.util.List; |
@@ -26,7 +26,7 @@ public record ModalConstraint(Modality modality, Constraint constraint) implemen | |||
26 | } | 26 | } |
27 | 27 | ||
28 | @Override | 28 | @Override |
29 | public LiteralReduction getReduction() { | 29 | public Reduction getReduction() { |
30 | return constraint.getReduction(); | 30 | return constraint.getReduction(); |
31 | } | 31 | } |
32 | 32 | ||