diff options
author | 2022-10-30 19:27:34 -0400 | |
---|---|---|
committer | 2022-11-05 19:41:17 +0100 | |
commit | 960af83c7c1cb871da03b9ac4ec6f44c94e78a1d (patch) | |
tree | 7d37ee007ee2d3b031d62ca892920d326758f438 /subprojects/store-query-viatra/src/main | |
parent | refactor: DNF query builder (diff) | |
download | refinery-960af83c7c1cb871da03b9ac4ec6f44c94e78a1d.tar.gz refinery-960af83c7c1cb871da03b9ac4ec6f44c94e78a1d.tar.zst refinery-960af83c7c1cb871da03b9ac4ec6f44c94e78a1d.zip |
refactor: DNF atoms
Restore count != capability.
Still needs semantics and tests for count atoms over partial models.
Diffstat (limited to 'subprojects/store-query-viatra/src/main')
4 files changed, 146 insertions, 36 deletions
diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/ViatraQueryableModelStore.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/ViatraQueryableModelStore.java index 702eb659..59fb1171 100644 --- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/ViatraQueryableModelStore.java +++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/ViatraQueryableModelStore.java | |||
@@ -4,12 +4,10 @@ import org.eclipse.viatra.query.runtime.api.GenericQuerySpecification; | |||
4 | import tools.refinery.store.model.ModelDiffCursor; | 4 | import tools.refinery.store.model.ModelDiffCursor; |
5 | import tools.refinery.store.model.ModelStore; | 5 | import tools.refinery.store.model.ModelStore; |
6 | import tools.refinery.store.model.ModelStoreImpl; | 6 | import tools.refinery.store.model.ModelStoreImpl; |
7 | import tools.refinery.store.model.RelationLike; | ||
7 | import tools.refinery.store.model.representation.DataRepresentation; | 8 | import tools.refinery.store.model.representation.DataRepresentation; |
8 | import tools.refinery.store.query.*; | 9 | import tools.refinery.store.query.*; |
9 | import tools.refinery.store.query.atom.DNFAtom; | 10 | import tools.refinery.store.query.atom.*; |
10 | import tools.refinery.store.query.atom.DNFCallAtom; | ||
11 | import tools.refinery.store.query.atom.EquivalenceAtom; | ||
12 | import tools.refinery.store.query.atom.RelationViewAtom; | ||
13 | import tools.refinery.store.query.viatra.internal.RawPatternMatcher; | 11 | import tools.refinery.store.query.viatra.internal.RawPatternMatcher; |
14 | import tools.refinery.store.query.viatra.internal.ViatraQueryableModel; | 12 | import tools.refinery.store.query.viatra.internal.ViatraQueryableModel; |
15 | import tools.refinery.store.query.viatra.internal.pquery.DNF2PQuery; | 13 | import tools.refinery.store.query.viatra.internal.pquery.DNF2PQuery; |
@@ -57,9 +55,11 @@ public class ViatraQueryableModelStore implements QueryableModelStore { | |||
57 | for (DNFAtom atom : clause.constraints()) { | 55 | for (DNFAtom atom : clause.constraints()) { |
58 | if (atom instanceof RelationViewAtom relationViewAtom) { | 56 | if (atom instanceof RelationViewAtom relationViewAtom) { |
59 | validateRelationAtom(relationViews, dnfPredicate, relationViewAtom); | 57 | validateRelationAtom(relationViews, dnfPredicate, relationViewAtom); |
60 | } else if (atom instanceof DNFCallAtom queryCallAtom) { | 58 | } else if (atom instanceof CallAtom<?> queryCallAtom) { |
61 | validatePredicateAtom(predicates, dnfPredicate, queryCallAtom); | 59 | validatePredicateAtom(predicates, dnfPredicate, queryCallAtom); |
62 | } else if (!(atom instanceof EquivalenceAtom)) { | 60 | } else if (atom instanceof CountNotEqualsAtom<?> countNotEqualsAtom) { |
61 | validateCountNotEqualsAtom(predicates, dnfPredicate, countNotEqualsAtom); | ||
62 | } else if (!(atom instanceof EquivalenceAtom || atom instanceof ConstantAtom)) { | ||
63 | throw new IllegalArgumentException("Unknown constraint: " + atom.toString()); | 63 | throw new IllegalArgumentException("Unknown constraint: " + atom.toString()); |
64 | } | 64 | } |
65 | } | 65 | } |
@@ -77,16 +77,24 @@ public class ViatraQueryableModelStore implements QueryableModelStore { | |||
77 | } | 77 | } |
78 | } | 78 | } |
79 | 79 | ||
80 | private void validatePredicateAtom(Set<DNF> predicates, DNF dnfPredicate, | 80 | private void validatePredicateReference(Set<DNF> predicates, DNF dnfPredicate, RelationLike target) { |
81 | DNFCallAtom queryCallAtom) { | 81 | if (!(target instanceof DNF dnfTarget) || !predicates.contains(dnfTarget)) { |
82 | if (!predicates.contains(queryCallAtom.getTarget())) { | ||
83 | throw new IllegalArgumentException( | 82 | throw new IllegalArgumentException( |
84 | "%s %s contains reference to a predicate %s that is not in the model.".formatted( | 83 | "%s %s contains reference to a predicate %s that is not in the model.".formatted( |
85 | DNF.class.getSimpleName(), dnfPredicate.getUniqueName(), | 84 | DNF.class.getSimpleName(), dnfPredicate.getUniqueName(), target.getName())); |
86 | queryCallAtom.getTarget().getName())); | ||
87 | } | 85 | } |
88 | } | 86 | } |
89 | 87 | ||
88 | private void validatePredicateAtom(Set<DNF> predicates, DNF dnfPredicate, CallAtom<?> queryCallAtom) { | ||
89 | validatePredicateReference(predicates, dnfPredicate, queryCallAtom.getTarget()); | ||
90 | } | ||
91 | |||
92 | private void validateCountNotEqualsAtom(Set<DNF> predicates, DNF dnfPredicate, | ||
93 | CountNotEqualsAtom<?> countNotEqualsAtom) { | ||
94 | validatePredicateReference(predicates, dnfPredicate, countNotEqualsAtom.mayTarget()); | ||
95 | validatePredicateReference(predicates, dnfPredicate, countNotEqualsAtom.mustTarget()); | ||
96 | } | ||
97 | |||
90 | private Map<DNF, GenericQuerySpecification<RawPatternMatcher>> initPredicates(Set<DNF> predicates) { | 98 | private Map<DNF, GenericQuerySpecification<RawPatternMatcher>> initPredicates(Set<DNF> predicates) { |
91 | Map<DNF, GenericQuerySpecification<RawPatternMatcher>> result = new HashMap<>(); | 99 | Map<DNF, GenericQuerySpecification<RawPatternMatcher>> result = new HashMap<>(); |
92 | var dnf2PQuery = new DNF2PQuery(); | 100 | var dnf2PQuery = new DNF2PQuery(); |
diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/CountExpressionEvaluator.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/CountExpressionEvaluator.java new file mode 100644 index 00000000..6fc96c05 --- /dev/null +++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/CountExpressionEvaluator.java | |||
@@ -0,0 +1,38 @@ | |||
1 | package tools.refinery.store.query.viatra.internal.pquery; | ||
2 | |||
3 | import org.eclipse.viatra.query.runtime.matchers.psystem.IExpressionEvaluator; | ||
4 | import org.eclipse.viatra.query.runtime.matchers.psystem.IValueProvider; | ||
5 | import tools.refinery.store.query.atom.ComparisonOperator; | ||
6 | import tools.refinery.store.query.atom.CountCallKind; | ||
7 | |||
8 | import java.util.List; | ||
9 | |||
10 | public record CountExpressionEvaluator(String variableName, ComparisonOperator operator, | ||
11 | int threshold) implements IExpressionEvaluator { | ||
12 | public CountExpressionEvaluator(String variableName, CountCallKind callKind) { | ||
13 | this(variableName, callKind.operator(), callKind.threshold()); | ||
14 | } | ||
15 | |||
16 | @Override | ||
17 | public String getShortDescription() { | ||
18 | return "%s %s %d".formatted(variableName, operator, threshold); | ||
19 | } | ||
20 | |||
21 | @Override | ||
22 | public Iterable<String> getInputParameterNames() { | ||
23 | return List.of(variableName); | ||
24 | } | ||
25 | |||
26 | @Override | ||
27 | public Object evaluateExpression(IValueProvider provider) { | ||
28 | int value = (Integer) provider.getValue(variableName); | ||
29 | return switch (operator) { | ||
30 | case EQUALS -> value == threshold; | ||
31 | case NOT_EQUALS -> value != threshold; | ||
32 | case LESS -> value < threshold; | ||
33 | case LESS_EQUALS -> value <= threshold; | ||
34 | case GREATER -> value > threshold; | ||
35 | case GREATER_EQUALS -> value >= threshold; | ||
36 | }; | ||
37 | } | ||
38 | } | ||
diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/CountNotEqualsExpressionEvaluator.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/CountNotEqualsExpressionEvaluator.java new file mode 100644 index 00000000..6f333a06 --- /dev/null +++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/CountNotEqualsExpressionEvaluator.java | |||
@@ -0,0 +1,30 @@ | |||
1 | package tools.refinery.store.query.viatra.internal.pquery; | ||
2 | |||
3 | import org.eclipse.viatra.query.runtime.matchers.psystem.IExpressionEvaluator; | ||
4 | import org.eclipse.viatra.query.runtime.matchers.psystem.IValueProvider; | ||
5 | |||
6 | import java.util.List; | ||
7 | |||
8 | public record CountNotEqualsExpressionEvaluator(boolean must, int threshold, String mayVariableName, | ||
9 | String mustVariableName) implements IExpressionEvaluator { | ||
10 | @Override | ||
11 | public String getShortDescription() { | ||
12 | return "%d %s not in [%s; %s]".formatted(threshold, must ? "must" : "may", mustVariableName, mayVariableName); | ||
13 | } | ||
14 | |||
15 | @Override | ||
16 | public Iterable<String> getInputParameterNames() { | ||
17 | return List.of(mayVariableName, mustVariableName); | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public Object evaluateExpression(IValueProvider provider) throws Exception { | ||
22 | int mayCount = (Integer) provider.getValue(mayVariableName); | ||
23 | int mustCount = (Integer) provider.getValue(mustVariableName); | ||
24 | if (must) { | ||
25 | return mayCount < threshold || mustCount > threshold; | ||
26 | } else { | ||
27 | return mayCount > threshold || mustCount < threshold; | ||
28 | } | ||
29 | } | ||
30 | } | ||
diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/DNF2PQuery.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/DNF2PQuery.java index e3c586a0..61b984ae 100644 --- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/DNF2PQuery.java +++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/DNF2PQuery.java | |||
@@ -2,20 +2,16 @@ package tools.refinery.store.query.viatra.internal.pquery; | |||
2 | 2 | ||
3 | import org.eclipse.viatra.query.runtime.matchers.psystem.PBody; | 3 | import org.eclipse.viatra.query.runtime.matchers.psystem.PBody; |
4 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable; | 4 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable; |
5 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality; | 5 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.*; |
6 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter; | ||
7 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality; | ||
8 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall; | ||
9 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure; | 6 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure; |
7 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue; | ||
10 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall; | 8 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall; |
11 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint; | 9 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint; |
12 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter; | 10 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter; |
11 | import org.eclipse.viatra.query.runtime.matchers.tuple.Tuple; | ||
13 | import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples; | 12 | import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples; |
14 | import tools.refinery.store.query.*; | 13 | import tools.refinery.store.query.*; |
15 | import tools.refinery.store.query.atom.DNFAtom; | 14 | import tools.refinery.store.query.atom.*; |
16 | import tools.refinery.store.query.atom.EquivalenceAtom; | ||
17 | import tools.refinery.store.query.atom.DNFCallAtom; | ||
18 | import tools.refinery.store.query.atom.RelationViewAtom; | ||
19 | import tools.refinery.store.query.view.RelationView; | 15 | import tools.refinery.store.query.view.RelationView; |
20 | 16 | ||
21 | import java.util.*; | 17 | import java.util.*; |
@@ -85,8 +81,12 @@ public class DNF2PQuery { | |||
85 | translateEquivalenceAtom(equivalenceAtom, body); | 81 | translateEquivalenceAtom(equivalenceAtom, body); |
86 | } else if (constraint instanceof RelationViewAtom relationViewAtom) { | 82 | } else if (constraint instanceof RelationViewAtom relationViewAtom) { |
87 | translateRelationViewAtom(relationViewAtom, body); | 83 | translateRelationViewAtom(relationViewAtom, body); |
88 | } else if (constraint instanceof DNFCallAtom dnfCallAtom) { | 84 | } else if (constraint instanceof CallAtom<?> callAtom) { |
89 | translateDNFCallAtom(dnfCallAtom, body); | 85 | translateCallAtom(callAtom, body); |
86 | } else if (constraint instanceof ConstantAtom constantAtom) { | ||
87 | translateConstantAtom(constantAtom, body); | ||
88 | } else if (constraint instanceof CountNotEqualsAtom<?> countNotEqualsAtom) { | ||
89 | translateCountNotEqualsAtom(countNotEqualsAtom, body); | ||
90 | } else { | 90 | } else { |
91 | throw new IllegalArgumentException("Unknown constraint: " + constraint.toString()); | 91 | throw new IllegalArgumentException("Unknown constraint: " + constraint.toString()); |
92 | } | 92 | } |
@@ -103,32 +103,66 @@ public class DNF2PQuery { | |||
103 | } | 103 | } |
104 | 104 | ||
105 | private void translateRelationViewAtom(RelationViewAtom relationViewAtom, PBody body) { | 105 | private void translateRelationViewAtom(RelationViewAtom relationViewAtom, PBody body) { |
106 | int arity = relationViewAtom.getSubstitution().size(); | 106 | new TypeConstraint(body, translateSubstitution(relationViewAtom.getSubstitution(), body), |
107 | wrapView(relationViewAtom.getTarget())); | ||
108 | } | ||
109 | |||
110 | private static Tuple translateSubstitution(List<Variable> substitution, PBody body) { | ||
111 | int arity = substitution.size(); | ||
107 | Object[] variables = new Object[arity]; | 112 | Object[] variables = new Object[arity]; |
108 | for (int i = 0; i < arity; i++) { | 113 | for (int i = 0; i < arity; i++) { |
109 | var variable = relationViewAtom.getSubstitution().get(i); | 114 | var variable = substitution.get(i); |
110 | variables[i] = body.getOrCreateVariableByName(variable.getUniqueName()); | 115 | variables[i] = body.getOrCreateVariableByName(variable.getUniqueName()); |
111 | } | 116 | } |
112 | new TypeConstraint(body, Tuples.flatTupleOf(variables), wrapView(relationViewAtom.getTarget())); | 117 | return Tuples.flatTupleOf(variables); |
113 | } | 118 | } |
114 | 119 | ||
115 | private RelationViewWrapper wrapView(RelationView<?> relationView) { | 120 | private RelationViewWrapper wrapView(RelationView<?> relationView) { |
116 | return view2WrapperMap.computeIfAbsent(relationView, RelationViewWrapper::new); | 121 | return view2WrapperMap.computeIfAbsent(relationView, RelationViewWrapper::new); |
117 | } | 122 | } |
118 | 123 | ||
119 | private void translateDNFCallAtom(DNFCallAtom queryCallAtom, PBody body) { | 124 | private void translateCallAtom(CallAtom<?> callAtom, PBody body) { |
120 | int arity = queryCallAtom.getSubstitution().size(); | 125 | if (!(callAtom.getTarget() instanceof DNF target)) { |
121 | Object[] variables = new Object[arity]; | 126 | throw new IllegalArgumentException("Only calls to DNF are supported"); |
122 | for (int i = 0; i < arity; i++) { | 127 | } |
123 | var variable = queryCallAtom.getSubstitution().get(i); | 128 | var variablesTuple = translateSubstitution(callAtom.getSubstitution(), body); |
124 | variables[i] = body.getOrCreateVariableByName(variable.getUniqueName()); | 129 | var translatedReferred = translate(target); |
130 | var callKind = callAtom.getKind(); | ||
131 | if (callKind instanceof BasicCallKind basicCallKind) { | ||
132 | switch (basicCallKind) { | ||
133 | case POSITIVE -> new PositivePatternCall(body, variablesTuple, translatedReferred); | ||
134 | case TRANSITIVE -> new BinaryTransitiveClosure(body, variablesTuple, translatedReferred); | ||
135 | case NEGATIVE -> new NegativePatternCall(body, variablesTuple, translatedReferred); | ||
136 | default -> throw new IllegalArgumentException("Unknown BasicCallKind: " + basicCallKind); | ||
137 | } | ||
138 | } else if (callKind instanceof CountCallKind countCallKind) { | ||
139 | var countVariableName = DNFUtils.generateUniqueName("count"); | ||
140 | var countPVariable = body.getOrCreateVariableByName(countVariableName); | ||
141 | new PatternMatchCounter(body, variablesTuple, translatedReferred, countPVariable); | ||
142 | new ExpressionEvaluation(body, new CountExpressionEvaluator(countVariableName, countCallKind), null); | ||
143 | } else { | ||
144 | throw new IllegalArgumentException("Unknown CallKind: " + callKind); | ||
125 | } | 145 | } |
126 | var variablesTuple = Tuples.flatTupleOf(variables); | 146 | } |
127 | var translatedReferred = translate(queryCallAtom.getTarget()); | 147 | |
128 | switch (queryCallAtom.getKind()) { | 148 | private void translateConstantAtom(ConstantAtom constantAtom, PBody body) { |
129 | case POSITIVE -> new PositivePatternCall(body, variablesTuple, translatedReferred); | 149 | var variable = body.getOrCreateVariableByName(constantAtom.variable().getUniqueName()); |
130 | case TRANSITIVE -> new BinaryTransitiveClosure(body, variablesTuple, translatedReferred); | 150 | new ConstantValue(body, variable, constantAtom.nodeId()); |
131 | case NEGATIVE -> new NegativePatternCall(body, variablesTuple, translatedReferred); | 151 | } |
152 | |||
153 | private void translateCountNotEqualsAtom(CountNotEqualsAtom<?> countNotEqualsAtom, PBody body) { | ||
154 | if (!(countNotEqualsAtom.mayTarget() instanceof DNF mayTarget) || | ||
155 | !(countNotEqualsAtom.mustTarget() instanceof DNF mustTarget)) { | ||
156 | throw new IllegalArgumentException("Only calls to DNF are supported"); | ||
132 | } | 157 | } |
158 | var variablesTuple = translateSubstitution(countNotEqualsAtom.substitution(), body); | ||
159 | var mayCountName = DNFUtils.generateUniqueName("countMay"); | ||
160 | var mayCountVariable = body.getOrCreateVariableByName(mayCountName); | ||
161 | new PatternMatchCounter(body, variablesTuple, translate(mayTarget), mayCountVariable); | ||
162 | var mustCountName = DNFUtils.generateUniqueName("countMust"); | ||
163 | var mustCountVariable = body.getOrCreateVariableByName(mustCountName); | ||
164 | new PatternMatchCounter(body, variablesTuple, translate(mustTarget), mustCountVariable); | ||
165 | new ExpressionEvaluation(body, new CountNotEqualsExpressionEvaluator(countNotEqualsAtom.must(), | ||
166 | countNotEqualsAtom.threshold(), mayCountName, mustCountName), null); | ||
133 | } | 167 | } |
134 | } | 168 | } |