1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
|
/*
* SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
*
* SPDX-License-Identifier: EPL-2.0
*/
package tools.refinery.store.query.viatra.internal.pquery;
import org.eclipse.viatra.query.runtime.matchers.context.IInputKey;
import org.eclipse.viatra.query.runtime.matchers.psystem.PBody;
import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable;
import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter;
import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall;
import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint;
import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter;
import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery;
import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PVisibility;
import org.eclipse.viatra.query.runtime.matchers.tuple.Tuple;
import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples;
import tools.refinery.store.query.Constraint;
import tools.refinery.store.query.dnf.Dnf;
import tools.refinery.store.query.dnf.DnfUtils;
import tools.refinery.store.query.literal.AbstractCallLiteral;
import tools.refinery.store.query.term.ParameterDirection;
import tools.refinery.store.query.term.Variable;
import tools.refinery.store.query.view.AnySymbolView;
import tools.refinery.store.query.view.SymbolView;
import tools.refinery.store.util.CycleDetectingMapper;
import java.util.*;
import java.util.function.ToIntFunction;
class QueryWrapperFactory {
private final Dnf2PQuery dnf2PQuery;
private final Map<AnySymbolView, SymbolViewWrapper> view2WrapperMap = new LinkedHashMap<>();
private final CycleDetectingMapper<RemappedConstraint, RawPQuery> wrapConstraint = new CycleDetectingMapper<>(
RemappedConstraint::toString, this::doWrapConstraint);
QueryWrapperFactory(Dnf2PQuery dnf2PQuery) {
this.dnf2PQuery = dnf2PQuery;
}
public PQuery wrapSymbolViewIdentityArguments(AnySymbolView symbolView) {
var identity = new int[symbolView.arity()];
for (int i = 0; i < identity.length; i++) {
identity[i] = i;
}
return maybeWrapConstraint(symbolView, identity);
}
public WrappedCall maybeWrapConstraint(AbstractCallLiteral callLiteral) {
var arguments = callLiteral.getArguments();
int arity = arguments.size();
var remappedParameters = new int[arity];
var unboundVariableIndices = new HashMap<Variable, Integer>();
var appendVariable = new VariableAppender();
for (int i = 0; i < arity; i++) {
var variable = arguments.get(i);
// Unify all variables to avoid VIATRA bugs, even if they're bound in the containing clause.
remappedParameters[i] = unboundVariableIndices.computeIfAbsent(variable, appendVariable::applyAsInt);
}
var pattern = maybeWrapConstraint(callLiteral.getTarget(), remappedParameters);
return new WrappedCall(pattern, appendVariable.getRemappedArguments());
}
private PQuery maybeWrapConstraint(Constraint constraint, int[] remappedParameters) {
if (remappedParameters.length != constraint.arity()) {
throw new IllegalArgumentException("Constraint %s expected %d parameters, but got %d parameters".formatted(
constraint, constraint.arity(), remappedParameters.length));
}
if (constraint instanceof Dnf dnf && isIdentity(remappedParameters)) {
return dnf2PQuery.translate(dnf);
}
return wrapConstraint.map(new RemappedConstraint(constraint, remappedParameters));
}
private static boolean isIdentity(int[] remappedParameters) {
for (int i = 0; i < remappedParameters.length; i++) {
if (remappedParameters[i] != i) {
return false;
}
}
return true;
}
private RawPQuery doWrapConstraint(RemappedConstraint remappedConstraint) {
var constraint = remappedConstraint.constraint();
var remappedParameters = remappedConstraint.remappedParameters();
checkNoInputParameters(constraint);
var embeddedPQuery = new RawPQuery(DnfUtils.generateUniqueName(constraint.name()), PVisibility.EMBEDDED);
var body = new PBody(embeddedPQuery);
int arity = Arrays.stream(remappedParameters).max().orElse(-1) + 1;
var parameters = new ArrayList<PParameter>(arity);
var parameterVariables = new PVariable[arity];
var symbolicParameters = new ArrayList<ExportedParameter>(arity);
for (int i = 0; i < arity; i++) {
var parameterName = "p" + i;
var parameter = new PParameter(parameterName);
parameters.add(parameter);
var variable = body.getOrCreateVariableByName(parameterName);
parameterVariables[i] = variable;
symbolicParameters.add(new ExportedParameter(body, variable, parameter));
}
embeddedPQuery.setParameters(parameters);
body.setSymbolicParameters(symbolicParameters);
var arguments = new Object[remappedParameters.length];
for (int i = 0; i < remappedParameters.length; i++) {
arguments[i] = parameterVariables[remappedParameters[i]];
}
var argumentTuple = Tuples.flatTupleOf(arguments);
addPositiveConstraint(constraint, body, argumentTuple);
embeddedPQuery.addBody(body);
return embeddedPQuery;
}
private static void checkNoInputParameters(Constraint constraint) {
for (var constraintParameter : constraint.getParameters()) {
if (constraintParameter.getDirection() == ParameterDirection.IN) {
throw new IllegalArgumentException("Input parameter %s of %s is not supported"
.formatted(constraintParameter, constraint));
}
}
}
private void addPositiveConstraint(Constraint constraint, PBody body, Tuple argumentTuple) {
if (constraint instanceof SymbolView<?> view) {
new TypeConstraint(body, argumentTuple, getInputKey(view));
} else if (constraint instanceof Dnf dnf) {
var calledPQuery = dnf2PQuery.translate(dnf);
new PositivePatternCall(body, argumentTuple, calledPQuery);
} else {
throw new IllegalArgumentException("Unknown Constraint: " + constraint);
}
}
public IInputKey getInputKey(AnySymbolView symbolView) {
return view2WrapperMap.computeIfAbsent(symbolView, SymbolViewWrapper::new);
}
public Map<AnySymbolView, IInputKey> getSymbolViews() {
return Collections.unmodifiableMap(view2WrapperMap);
}
public record WrappedCall(PQuery pattern, List<Variable> remappedArguments) {
}
private static class VariableAppender implements ToIntFunction<Variable> {
private final List<Variable> remappedArguments = new ArrayList<>();
private int nextIndex = 0;
@Override
public int applyAsInt(Variable variable) {
remappedArguments.add(variable);
int index = nextIndex;
nextIndex++;
return index;
}
public List<Variable> getRemappedArguments() {
return remappedArguments;
}
}
private record RemappedConstraint(Constraint constraint, int[] remappedParameters) {
@Override
public boolean equals(Object o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
RemappedConstraint that = (RemappedConstraint) o;
return constraint.equals(that.constraint) && Arrays.equals(remappedParameters, that.remappedParameters);
}
@Override
public int hashCode() {
int result = Objects.hash(constraint);
result = 31 * result + Arrays.hashCode(remappedParameters);
return result;
}
@Override
public String toString() {
return "RemappedConstraint{constraint=%s, remappedParameters=%s}".formatted(constraint,
Arrays.toString(remappedParameters));
}
}
}
|
