diff options
author | 2023-07-09 19:53:46 +0200 | |
---|---|---|
committer | 2023-07-09 19:53:46 +0200 | |
commit | f6440ff43e2e7497116c2cf762f61e07834b229f (patch) | |
tree | 0c5719408fcf061aa72781424af1002d6bbabe39 /subprojects/store-query | |
parent | refactor: Dnf lifter (diff) | |
download | refinery-f6440ff43e2e7497116c2cf762f61e07834b229f.tar.gz refinery-f6440ff43e2e7497116c2cf762f61e07834b229f.tar.zst refinery-f6440ff43e2e7497116c2cf762f61e07834b229f.zip |
refactor: enable data variable unification
This is needed for demand set transformation of DNFs with input data parameters,
where the result of the transformation has an out data parameter that has to be
unified with the variable in the parent clause.
Diffstat (limited to 'subprojects/store-query')
9 files changed, 37 insertions, 245 deletions
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 f2749094..5d77b9aa 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 | |||
@@ -11,7 +11,6 @@ import tools.refinery.store.query.literal.*; | |||
11 | import tools.refinery.store.query.substitution.MapBasedSubstitution; | 11 | import tools.refinery.store.query.substitution.MapBasedSubstitution; |
12 | import tools.refinery.store.query.substitution.StatelessSubstitution; | 12 | import tools.refinery.store.query.substitution.StatelessSubstitution; |
13 | import tools.refinery.store.query.substitution.Substitution; | 13 | import tools.refinery.store.query.substitution.Substitution; |
14 | import tools.refinery.store.query.term.NodeVariable; | ||
15 | import tools.refinery.store.query.term.ParameterDirection; | 14 | import tools.refinery.store.query.term.ParameterDirection; |
16 | import tools.refinery.store.query.term.Variable; | 15 | import tools.refinery.store.query.term.Variable; |
17 | 16 | ||
@@ -21,8 +20,8 @@ import java.util.function.Function; | |||
21 | class ClausePostProcessor { | 20 | class ClausePostProcessor { |
22 | private final Map<Variable, ParameterInfo> parameters; | 21 | private final Map<Variable, ParameterInfo> parameters; |
23 | private final List<Literal> literals; | 22 | private final List<Literal> literals; |
24 | private final Map<NodeVariable, NodeVariable> representatives = new LinkedHashMap<>(); | 23 | private final Map<Variable, Variable> representatives = new LinkedHashMap<>(); |
25 | private final Map<NodeVariable, Set<NodeVariable>> equivalencePartition = new HashMap<>(); | 24 | private final Map<Variable, Set<Variable>> equivalencePartition = new HashMap<>(); |
26 | private List<Literal> substitutedLiterals; | 25 | private List<Literal> substitutedLiterals; |
27 | private final Set<Variable> existentiallyQuantifiedVariables = new LinkedHashSet<>(); | 26 | private final Set<Variable> existentiallyQuantifiedVariables = new LinkedHashSet<>(); |
28 | private Set<Variable> positiveVariables; | 27 | private Set<Variable> positiveVariables; |
@@ -78,7 +77,7 @@ class ClausePostProcessor { | |||
78 | return literal instanceof EquivalenceLiteral equivalenceLiteral && equivalenceLiteral.isPositive(); | 77 | return literal instanceof EquivalenceLiteral equivalenceLiteral && equivalenceLiteral.isPositive(); |
79 | } | 78 | } |
80 | 79 | ||
81 | private void mergeVariables(NodeVariable left, NodeVariable right) { | 80 | private void mergeVariables(Variable left, Variable right) { |
82 | var leftRepresentative = getRepresentative(left); | 81 | var leftRepresentative = getRepresentative(left); |
83 | var rightRepresentative = getRepresentative(right); | 82 | var rightRepresentative = getRepresentative(right); |
84 | var leftInfo = parameters.get(leftRepresentative); | 83 | var leftInfo = parameters.get(leftRepresentative); |
@@ -91,7 +90,7 @@ class ClausePostProcessor { | |||
91 | } | 90 | } |
92 | } | 91 | } |
93 | 92 | ||
94 | private void doMergeVariables(NodeVariable parentRepresentative, NodeVariable newChildRepresentative) { | 93 | private void doMergeVariables(Variable parentRepresentative, Variable newChildRepresentative) { |
95 | var parentSet = getEquivalentVariables(parentRepresentative); | 94 | var parentSet = getEquivalentVariables(parentRepresentative); |
96 | var childSet = getEquivalentVariables(newChildRepresentative); | 95 | var childSet = getEquivalentVariables(newChildRepresentative); |
97 | parentSet.addAll(childSet); | 96 | parentSet.addAll(childSet); |
@@ -101,18 +100,18 @@ class ClausePostProcessor { | |||
101 | } | 100 | } |
102 | } | 101 | } |
103 | 102 | ||
104 | private NodeVariable getRepresentative(NodeVariable variable) { | 103 | private Variable getRepresentative(Variable variable) { |
105 | return representatives.computeIfAbsent(variable, Function.identity()); | 104 | return representatives.computeIfAbsent(variable, Function.identity()); |
106 | } | 105 | } |
107 | 106 | ||
108 | private Set<NodeVariable> getEquivalentVariables(NodeVariable variable) { | 107 | private Set<Variable> getEquivalentVariables(Variable variable) { |
109 | var representative = getRepresentative(variable); | 108 | var representative = getRepresentative(variable); |
110 | if (!representative.equals(variable)) { | 109 | if (!representative.equals(variable)) { |
111 | throw new AssertionError("NodeVariable %s already has a representative %s" | 110 | throw new AssertionError("NodeVariable %s already has a representative %s" |
112 | .formatted(variable, representative)); | 111 | .formatted(variable, representative)); |
113 | } | 112 | } |
114 | return equivalencePartition.computeIfAbsent(variable, key -> { | 113 | return equivalencePartition.computeIfAbsent(variable, key -> { |
115 | var set = new HashSet<NodeVariable>(1); | 114 | var set = new HashSet<Variable>(1); |
116 | set.add(key); | 115 | set.add(key); |
117 | return set; | 116 | return set; |
118 | }); | 117 | }); |
@@ -123,7 +122,7 @@ class ClausePostProcessor { | |||
123 | var left = pair.getKey(); | 122 | var left = pair.getKey(); |
124 | var right = pair.getValue(); | 123 | var right = pair.getValue(); |
125 | if (!left.equals(right) && parameters.containsKey(left) && parameters.containsKey(right)) { | 124 | if (!left.equals(right) && parameters.containsKey(left) && parameters.containsKey(right)) { |
126 | substitutedLiterals.add(left.isEquivalent(right)); | 125 | substitutedLiterals.add(new EquivalenceLiteral(true, left, right)); |
127 | } | 126 | } |
128 | } | 127 | } |
129 | } | 128 | } |
@@ -149,20 +148,7 @@ class ClausePostProcessor { | |||
149 | 148 | ||
150 | private void computeExistentiallyQuantifiedVariables() { | 149 | private void computeExistentiallyQuantifiedVariables() { |
151 | for (var literal : substitutedLiterals) { | 150 | for (var literal : substitutedLiterals) { |
152 | for (var variable : literal.getOutputVariables()) { | 151 | existentiallyQuantifiedVariables.addAll(literal.getOutputVariables()); |
153 | boolean added = existentiallyQuantifiedVariables.add(variable); | ||
154 | if (!variable.isUnifiable()) { | ||
155 | var parameterInfo = parameters.get(variable); | ||
156 | if (parameterInfo != null && parameterInfo.direction() == ParameterDirection.IN) { | ||
157 | throw new IllegalArgumentException("Trying to bind %s parameter %s" | ||
158 | .formatted(ParameterDirection.IN, variable)); | ||
159 | } | ||
160 | if (!added) { | ||
161 | throw new IllegalArgumentException("Variable %s has multiple assigned values" | ||
162 | .formatted(variable)); | ||
163 | } | ||
164 | } | ||
165 | } | ||
166 | } | 152 | } |
167 | } | 153 | } |
168 | 154 | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/SymbolicParameter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/SymbolicParameter.java index 1e96cf27..fe9cefcc 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/SymbolicParameter.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/SymbolicParameter.java | |||
@@ -24,10 +24,6 @@ public final class SymbolicParameter extends Parameter { | |||
24 | return variable; | 24 | return variable; |
25 | } | 25 | } |
26 | 26 | ||
27 | public boolean isUnifiable() { | ||
28 | return variable.isUnifiable(); | ||
29 | } | ||
30 | |||
31 | public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) { | 27 | public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) { |
32 | return Objects.hash(super.hashCode(), helper.getVariableHashCode(variable)); | 28 | return Objects.hash(super.hashCode(), helper.getVariableHashCode(variable)); |
33 | } | 29 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java index a355dc3b..263c2e20 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java | |||
@@ -14,6 +14,8 @@ import tools.refinery.store.query.term.Variable; | |||
14 | 14 | ||
15 | import java.util.*; | 15 | import java.util.*; |
16 | 16 | ||
17 | // {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}. | ||
18 | @SuppressWarnings("squid:S2160") | ||
17 | public abstract class AbstractCallLiteral extends AbstractLiteral { | 19 | public abstract class AbstractCallLiteral extends AbstractLiteral { |
18 | private final Constraint target; | 20 | private final Constraint target; |
19 | private final List<Variable> arguments; | 21 | private final List<Variable> arguments; |
@@ -42,16 +44,12 @@ public abstract class AbstractCallLiteral extends AbstractLiteral { | |||
42 | } | 44 | } |
43 | switch (parameter.getDirection()) { | 45 | switch (parameter.getDirection()) { |
44 | case IN -> { | 46 | case IN -> { |
45 | if (mutableOutArguments.remove(argument)) { | 47 | mutableOutArguments.remove(argument); |
46 | checkInOutUnifiable(argument); | ||
47 | } | ||
48 | mutableInArguments.add(argument); | 48 | mutableInArguments.add(argument); |
49 | } | 49 | } |
50 | case OUT -> { | 50 | case OUT -> { |
51 | if (mutableInArguments.contains(argument)) { | 51 | if (!mutableInArguments.contains(argument)) { |
52 | checkInOutUnifiable(argument); | 52 | mutableOutArguments.add(argument); |
53 | } else if (!mutableOutArguments.add(argument)) { | ||
54 | checkDuplicateOutUnifiable(argument); | ||
55 | } | 53 | } |
56 | } | 54 | } |
57 | } | 55 | } |
@@ -60,19 +58,6 @@ public abstract class AbstractCallLiteral extends AbstractLiteral { | |||
60 | outArguments = Collections.unmodifiableSet(mutableOutArguments); | 58 | outArguments = Collections.unmodifiableSet(mutableOutArguments); |
61 | } | 59 | } |
62 | 60 | ||
63 | private static void checkInOutUnifiable(Variable argument) { | ||
64 | if (!argument.isUnifiable()) { | ||
65 | throw new IllegalArgumentException("Argument %s cannot appear with both %s and %s direction" | ||
66 | .formatted(argument, ParameterDirection.IN, ParameterDirection.OUT)); | ||
67 | } | ||
68 | } | ||
69 | |||
70 | private static void checkDuplicateOutUnifiable(Variable argument) { | ||
71 | if (!argument.isUnifiable()) { | ||
72 | throw new IllegalArgumentException("Argument %s cannot be bound multiple times".formatted(argument)); | ||
73 | } | ||
74 | } | ||
75 | |||
76 | public Constraint getTarget() { | 61 | public Constraint getTarget() { |
77 | return target; | 62 | return target; |
78 | } | 63 | } |
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 61b7344f..9a0c22d1 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 | |||
@@ -8,18 +8,23 @@ package tools.refinery.store.query.literal; | |||
8 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | 8 | import tools.refinery.store.query.equality.LiteralEqualityHelper; |
9 | import tools.refinery.store.query.equality.LiteralHashCodeHelper; | 9 | import tools.refinery.store.query.equality.LiteralHashCodeHelper; |
10 | import tools.refinery.store.query.substitution.Substitution; | 10 | import tools.refinery.store.query.substitution.Substitution; |
11 | import tools.refinery.store.query.term.NodeVariable; | ||
12 | import tools.refinery.store.query.term.Variable; | 11 | import tools.refinery.store.query.term.Variable; |
13 | 12 | ||
14 | import java.util.Objects; | 13 | import java.util.Objects; |
15 | import java.util.Set; | 14 | import java.util.Set; |
16 | 15 | ||
16 | // {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}. | ||
17 | @SuppressWarnings("squid:S2160") | ||
17 | public final class EquivalenceLiteral extends AbstractLiteral implements CanNegate<EquivalenceLiteral> { | 18 | public final class EquivalenceLiteral extends AbstractLiteral implements CanNegate<EquivalenceLiteral> { |
18 | private final boolean positive; | 19 | private final boolean positive; |
19 | private final NodeVariable left; | 20 | private final Variable left; |
20 | private final NodeVariable right; | 21 | private final Variable right; |
21 | 22 | ||
22 | public EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right) { | 23 | public EquivalenceLiteral(boolean positive, Variable left, Variable right) { |
24 | if (!left.tryGetType().equals(right.tryGetType())) { | ||
25 | throw new IllegalArgumentException("Variables %s and %s of different type cannot be equivalent" | ||
26 | .formatted(left, right)); | ||
27 | } | ||
23 | this.positive = positive; | 28 | this.positive = positive; |
24 | this.left = left; | 29 | this.left = left; |
25 | this.right = right; | 30 | this.right = right; |
@@ -29,11 +34,11 @@ public final class EquivalenceLiteral extends AbstractLiteral implements CanNega | |||
29 | return positive; | 34 | return positive; |
30 | } | 35 | } |
31 | 36 | ||
32 | public NodeVariable getLeft() { | 37 | public Variable getLeft() { |
33 | return left; | 38 | return left; |
34 | } | 39 | } |
35 | 40 | ||
36 | public NodeVariable getRight() { | 41 | public Variable getRight() { |
37 | return right; | 42 | return right; |
38 | } | 43 | } |
39 | 44 | ||
@@ -59,8 +64,8 @@ public final class EquivalenceLiteral extends AbstractLiteral implements CanNega | |||
59 | 64 | ||
60 | @Override | 65 | @Override |
61 | public EquivalenceLiteral substitute(Substitution substitution) { | 66 | public EquivalenceLiteral substitute(Substitution substitution) { |
62 | return new EquivalenceLiteral(positive, substitution.getTypeSafeSubstitute(left), | 67 | return new EquivalenceLiteral(positive, substitution.getSubstitute(left), |
63 | substitution.getTypeSafeSubstitute(right)); | 68 | substitution.getSubstitute(right)); |
64 | } | 69 | } |
65 | 70 | ||
66 | @Override | 71 | @Override |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java index ed6941da..4d88051b 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java | |||
@@ -47,11 +47,6 @@ public abstract sealed class AnyDataVariable extends Variable implements AnyTerm | |||
47 | } | 47 | } |
48 | 48 | ||
49 | @Override | 49 | @Override |
50 | public boolean isUnifiable() { | ||
51 | return false; | ||
52 | } | ||
53 | |||
54 | @Override | ||
55 | public abstract AnyDataVariable renew(@Nullable String name); | 50 | public abstract AnyDataVariable renew(@Nullable String name); |
56 | 51 | ||
57 | @Override | 52 | @Override |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java index e71c69ac..9b62e545 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java | |||
@@ -8,6 +8,7 @@ package tools.refinery.store.query.term; | |||
8 | import org.jetbrains.annotations.Nullable; | 8 | import org.jetbrains.annotations.Nullable; |
9 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | 9 | import tools.refinery.store.query.equality.LiteralEqualityHelper; |
10 | import tools.refinery.store.query.equality.LiteralHashCodeHelper; | 10 | import tools.refinery.store.query.equality.LiteralHashCodeHelper; |
11 | import tools.refinery.store.query.literal.EquivalenceLiteral; | ||
11 | import tools.refinery.store.query.literal.Literal; | 12 | import tools.refinery.store.query.literal.Literal; |
12 | import tools.refinery.store.query.substitution.Substitution; | 13 | import tools.refinery.store.query.substitution.Substitution; |
13 | import tools.refinery.store.query.valuation.Valuation; | 14 | import tools.refinery.store.query.valuation.Valuation; |
@@ -90,4 +91,12 @@ public final class DataVariable<T> extends AnyDataVariable implements Term<T> { | |||
90 | public int hashCode() { | 91 | public int hashCode() { |
91 | return Objects.hash(super.hashCode(), type); | 92 | return Objects.hash(super.hashCode(), type); |
92 | } | 93 | } |
94 | |||
95 | public EquivalenceLiteral isEquivalent(DataVariable<T> other) { | ||
96 | return new EquivalenceLiteral(true, this, other); | ||
97 | } | ||
98 | |||
99 | public EquivalenceLiteral notEquivalent(DataVariable<T> other) { | ||
100 | return new EquivalenceLiteral(false, this, other); | ||
101 | } | ||
93 | } | 102 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java index e466f1c9..2f9c8bf1 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java | |||
@@ -22,11 +22,6 @@ public final class NodeVariable extends Variable { | |||
22 | } | 22 | } |
23 | 23 | ||
24 | @Override | 24 | @Override |
25 | public boolean isUnifiable() { | ||
26 | return true; | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | public NodeVariable renew(@Nullable String name) { | 25 | public NodeVariable renew(@Nullable String name) { |
31 | return Variable.of(name); | 26 | return Variable.of(name); |
32 | } | 27 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java index 89ef0d89..1b553704 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java | |||
@@ -38,8 +38,6 @@ public abstract sealed class Variable permits AnyDataVariable, NodeVariable { | |||
38 | return uniqueName; | 38 | return uniqueName; |
39 | } | 39 | } |
40 | 40 | ||
41 | public abstract boolean isUnifiable(); | ||
42 | |||
43 | public abstract Variable renew(@Nullable String name); | 41 | public abstract Variable renew(@Nullable String name); |
44 | 42 | ||
45 | public abstract Variable renew(); | 43 | public abstract Variable renew(); |
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/VariableDirectionTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/VariableDirectionTest.java index c509da4d..bfeaa447 100644 --- a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/VariableDirectionTest.java +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/VariableDirectionTest.java | |||
@@ -28,9 +28,8 @@ import static org.hamcrest.Matchers.hasItem; | |||
28 | import static org.hamcrest.Matchers.not; | 28 | import static org.hamcrest.Matchers.not; |
29 | import static org.junit.jupiter.api.Assertions.assertDoesNotThrow; | 29 | import static org.junit.jupiter.api.Assertions.assertDoesNotThrow; |
30 | import static org.junit.jupiter.api.Assertions.assertThrows; | 30 | import static org.junit.jupiter.api.Assertions.assertThrows; |
31 | import static tools.refinery.store.query.literal.Literals.check; | ||
32 | import static tools.refinery.store.query.literal.Literals.not; | 31 | import static tools.refinery.store.query.literal.Literals.not; |
33 | import static tools.refinery.store.query.term.int_.IntTerms.*; | 32 | import static tools.refinery.store.query.term.int_.IntTerms.INT_SUM; |
34 | 33 | ||
35 | class VariableDirectionTest { | 34 | class VariableDirectionTest { |
36 | private static final Symbol<Boolean> person = Symbol.of("Person", 1); | 35 | private static final Symbol<Boolean> person = Symbol.of("Person", 1); |
@@ -246,182 +245,6 @@ class VariableDirectionTest { | |||
246 | ); | 245 | ); |
247 | } | 246 | } |
248 | 247 | ||
249 | @ParameterizedTest | ||
250 | @MethodSource("clausesWithDataVariableInput") | ||
251 | void unboundOutDataVariableTest(List<? extends Literal> clause) { | ||
252 | var builder = Dnf.builder().parameter(x, ParameterDirection.OUT).clause(clause); | ||
253 | assertThrows(IllegalArgumentException.class, builder::build); | ||
254 | } | ||
255 | |||
256 | @ParameterizedTest | ||
257 | @MethodSource("clausesWithDataVariableInput") | ||
258 | void unboundInDataVariableTest(List<? extends Literal> clause) { | ||
259 | var builder = Dnf.builder().parameter(x, ParameterDirection.IN).clause(clause); | ||
260 | var dnf = assertDoesNotThrow(builder::build); | ||
261 | var clauses = dnf.getClauses(); | ||
262 | if (clauses.size() > 0) { | ||
263 | assertThat(clauses.get(0).positiveVariables(), hasItem(x)); | ||
264 | } | ||
265 | } | ||
266 | |||
267 | @ParameterizedTest | ||
268 | @MethodSource("clausesWithDataVariableInput") | ||
269 | void boundPrivateDataVariableTest(List<? extends Literal> clause) { | ||
270 | var clauseWithBinding = new ArrayList<Literal>(clause); | ||
271 | clauseWithBinding.add(x.assign(constant(27))); | ||
272 | var builder = Dnf.builder().clause(clauseWithBinding); | ||
273 | var dnf = assertDoesNotThrow(builder::build); | ||
274 | var clauses = dnf.getClauses(); | ||
275 | if (clauses.size() > 0) { | ||
276 | assertThat(clauses.get(0).positiveVariables(), hasItem(x)); | ||
277 | } | ||
278 | } | ||
279 | |||
280 | static Stream<Arguments> clausesWithDataVariableInput() { | ||
281 | return Stream.concat( | ||
282 | clausesNotBindingDataVariable(), | ||
283 | literalToClauseArgumentStream(literalsWithRequiredDataVariableInput()) | ||
284 | ); | ||
285 | } | ||
286 | |||
287 | @ParameterizedTest | ||
288 | @MethodSource("clausesNotBindingDataVariable") | ||
289 | void unboundPrivateDataVariableTest(List<? extends Literal> clause) { | ||
290 | var builder = Dnf.builder().clause(clause); | ||
291 | var dnf = assertDoesNotThrow(builder::build); | ||
292 | var clauses = dnf.getClauses(); | ||
293 | if (clauses.size() > 0) { | ||
294 | assertThat(clauses.get(0).positiveVariables(), not(hasItem(x))); | ||
295 | } | ||
296 | } | ||
297 | |||
298 | static Stream<Arguments> clausesNotBindingDataVariable() { | ||
299 | return Stream.concat( | ||
300 | Stream.of( | ||
301 | Arguments.of(List.of()), | ||
302 | Arguments.of(List.of(BooleanLiteral.TRUE)), | ||
303 | Arguments.of(List.of(BooleanLiteral.FALSE)) | ||
304 | ), | ||
305 | literalToClauseArgumentStream(literalsWithPrivateDataVariable()) | ||
306 | ); | ||
307 | } | ||
308 | |||
309 | @ParameterizedTest | ||
310 | @MethodSource("literalsWithPrivateDataVariable") | ||
311 | void unboundTwicePrivateDataVariableTest(Literal literal) { | ||
312 | var builder = Dnf.builder().clause(not(ageView.call(p, x)), literal); | ||
313 | assertThrows(IllegalArgumentException.class, builder::build); | ||
314 | } | ||
315 | |||
316 | static Stream<Arguments> literalsWithPrivateDataVariable() { | ||
317 | var dnfWithOutput = Dnf.builder("WithDataOutput") | ||
318 | .parameter(y, ParameterDirection.OUT) | ||
319 | .parameter(q, ParameterDirection.OUT) | ||
320 | .clause(ageView.call(q, y)) | ||
321 | .build(); | ||
322 | |||
323 | return Stream.of( | ||
324 | Arguments.of(not(ageView.call(q, x))), | ||
325 | Arguments.of(y.assign(ageView.count(q, x))), | ||
326 | Arguments.of(not(dnfWithOutput.call(x, q))) | ||
327 | ); | ||
328 | } | ||
329 | |||
330 | @ParameterizedTest | ||
331 | @MethodSource("literalsWithRequiredDataVariableInput") | ||
332 | void unboundPrivateDataVariableTest(Literal literal) { | ||
333 | var builder = Dnf.builder().clause(literal); | ||
334 | assertThrows(IllegalArgumentException.class, builder::build); | ||
335 | } | ||
336 | |||
337 | static Stream<Arguments> literalsWithRequiredDataVariableInput() { | ||
338 | var dnfWithInput = Dnf.builder("WithDataInput") | ||
339 | .parameter(y, ParameterDirection.IN) | ||
340 | .parameter(q, ParameterDirection.OUT) | ||
341 | .clause(ageView.call(q, x)) | ||
342 | .build(); | ||
343 | // We are passing {@code y} to the parameter named {@code right} of {@code greaterEq}. | ||
344 | @SuppressWarnings("SuspiciousNameCombination") | ||
345 | var dnfWithInputToAggregate = Dnf.builder("WithDataInputToAggregate") | ||
346 | .parameter(y, ParameterDirection.IN) | ||
347 | .parameter(q, ParameterDirection.OUT) | ||
348 | .parameter(x, ParameterDirection.OUT) | ||
349 | .clause( | ||
350 | friendView.call(p, q), | ||
351 | ageView.call(q, x), | ||
352 | check(greaterEq(x, y)) | ||
353 | ) | ||
354 | .build(); | ||
355 | |||
356 | return Stream.of( | ||
357 | Arguments.of(dnfWithInput.call(x, q)), | ||
358 | Arguments.of(not(dnfWithInput.call(x, q))), | ||
359 | Arguments.of(y.assign(dnfWithInput.count(x, q))), | ||
360 | Arguments.of(y.assign(dnfWithInputToAggregate.aggregateBy(z, INT_SUM, x, q, z))) | ||
361 | ); | ||
362 | } | ||
363 | |||
364 | @ParameterizedTest | ||
365 | @MethodSource("literalsWithDataVariableOutput") | ||
366 | void boundDataParameterTest(Literal literal) { | ||
367 | var builder = Dnf.builder().parameter(x, ParameterDirection.OUT).clause(literal); | ||
368 | var dnf = assertDoesNotThrow(builder::build); | ||
369 | assertThat(dnf.getClauses().get(0).positiveVariables(), hasItem(x)); | ||
370 | } | ||
371 | |||
372 | @ParameterizedTest | ||
373 | @MethodSource("literalsWithDataVariableOutput") | ||
374 | void boundTwiceDataParameterTest(Literal literal) { | ||
375 | var builder = Dnf.builder().parameter(x, ParameterDirection.IN).clause(literal); | ||
376 | assertThrows(IllegalArgumentException.class, builder::build); | ||
377 | } | ||
378 | |||
379 | @ParameterizedTest | ||
380 | @MethodSource("literalsWithDataVariableOutput") | ||
381 | void boundPrivateDataVariableOutputTest(Literal literal) { | ||
382 | var dnfWithInput = Dnf.builder("WithInput") | ||
383 | .parameter(x, ParameterDirection.IN) | ||
384 | .clause(check(greaterEq(x, constant(24)))) | ||
385 | .build(); | ||
386 | var builder = Dnf.builder().clause(dnfWithInput.call(x), literal); | ||
387 | var dnf = assertDoesNotThrow(builder::build); | ||
388 | assertThat(dnf.getClauses().get(0).positiveVariables(), hasItem(x)); | ||
389 | } | ||
390 | |||
391 | @ParameterizedTest | ||
392 | @MethodSource("literalsWithDataVariableOutput") | ||
393 | void boundTwicePrivateDataVariableOutputTest(Literal literal) { | ||
394 | var builder = Dnf.builder().clause(x.assign(constant(27)), literal); | ||
395 | assertThrows(IllegalArgumentException.class, builder::build); | ||
396 | } | ||
397 | |||
398 | static Stream<Arguments> literalsWithDataVariableOutput() { | ||
399 | var dnfWithOutput = Dnf.builder("WithOutput") | ||
400 | .parameter(q, ParameterDirection.OUT) | ||
401 | .clause(personView.call(q)) | ||
402 | .build(); | ||
403 | var dnfWithDataOutput = Dnf.builder("WithDataOutput") | ||
404 | .parameter(y, ParameterDirection.OUT) | ||
405 | .parameter(q, ParameterDirection.OUT) | ||
406 | .clause(ageView.call(q, y)) | ||
407 | .build(); | ||
408 | var dnfWithOutputToAggregate = Dnf.builder("WithDataOutputToAggregate") | ||
409 | .parameter(q, ParameterDirection.OUT) | ||
410 | .parameter(y, ParameterDirection.OUT) | ||
411 | .clause(ageView.call(q, y)) | ||
412 | .build(); | ||
413 | |||
414 | return Stream.of( | ||
415 | Arguments.of(x.assign(constant(24))), | ||
416 | Arguments.of(ageView.call(q, x)), | ||
417 | Arguments.of(x.assign(personView.count(q))), | ||
418 | Arguments.of(x.assign(ageView.aggregate(INT_SUM, q))), | ||
419 | Arguments.of(dnfWithDataOutput.call(x, q)), | ||
420 | Arguments.of(x.assign(dnfWithOutput.count(q))), | ||
421 | Arguments.of(x.assign(dnfWithOutputToAggregate.aggregateBy(z, INT_SUM, q, z))) | ||
422 | ); | ||
423 | } | ||
424 | |||
425 | private static Stream<Arguments> literalToClauseArgumentStream(Stream<Arguments> literalArgumentsStream) { | 248 | private static Stream<Arguments> literalToClauseArgumentStream(Stream<Arguments> literalArgumentsStream) { |
426 | return literalArgumentsStream.map(arguments -> Arguments.of(List.of(arguments.get()[0]))); | 249 | return literalArgumentsStream.map(arguments -> Arguments.of(List.of(arguments.get()[0]))); |
427 | } | 250 | } |