diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-05-01 02:07:23 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-05-01 02:42:34 +0200 |
commit | 4e698774925468062974b990143c1091e23ed63b (patch) | |
tree | 21f2fc38b6b3b5f3be6ecbdee100d385a2e92c05 /subprojects | |
parent | fix(web): editor cursor styling (diff) | |
download | refinery-4e698774925468062974b990143c1091e23ed63b.tar.gz refinery-4e698774925468062974b990143c1091e23ed63b.tar.zst refinery-4e698774925468062974b990143c1091e23ed63b.zip |
feat: query parameter binding validation
* Introduce parameter directions for constraints and DNF
* Introduce variable directions for literals
* Infer and check variable directions in DNF and topologically sort literals by
their input variables
Diffstat (limited to 'subprojects')
49 files changed, 1595 insertions, 446 deletions
diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/context/RelationalQueryMetaContext.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/context/RelationalQueryMetaContext.java index cf96b7fd..211eacb4 100644 --- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/context/RelationalQueryMetaContext.java +++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/context/RelationalQueryMetaContext.java | |||
@@ -9,7 +9,6 @@ import org.eclipse.viatra.query.runtime.matchers.context.AbstractQueryMetaContex | |||
9 | import org.eclipse.viatra.query.runtime.matchers.context.IInputKey; | 9 | import org.eclipse.viatra.query.runtime.matchers.context.IInputKey; |
10 | import org.eclipse.viatra.query.runtime.matchers.context.InputKeyImplication; | 10 | import org.eclipse.viatra.query.runtime.matchers.context.InputKeyImplication; |
11 | import org.eclipse.viatra.query.runtime.matchers.context.common.JavaTransitiveInstancesKey; | 11 | import org.eclipse.viatra.query.runtime.matchers.context.common.JavaTransitiveInstancesKey; |
12 | import tools.refinery.store.query.term.DataSort; | ||
13 | import tools.refinery.store.query.viatra.internal.pquery.SymbolViewWrapper; | 12 | import tools.refinery.store.query.viatra.internal.pquery.SymbolViewWrapper; |
14 | import tools.refinery.store.query.view.AnySymbolView; | 13 | import tools.refinery.store.query.view.AnySymbolView; |
15 | 14 | ||
@@ -62,14 +61,14 @@ public class RelationalQueryMetaContext extends AbstractQueryMetaContext { | |||
62 | relationViewImplication.impliedIndices())); | 61 | relationViewImplication.impliedIndices())); |
63 | } | 62 | } |
64 | } | 63 | } |
65 | var sorts = symbolView.getSorts(); | 64 | var parameters = symbolView.getParameters(); |
66 | int arity = symbolView.arity(); | 65 | int arity = symbolView.arity(); |
67 | for (int i = 0; i < arity; i++) { | 66 | for (int i = 0; i < arity; i++) { |
68 | var sort = sorts.get(i); | 67 | var parameter = parameters.get(i); |
69 | if (sort instanceof DataSort<?> dataSort) { | 68 | var parameterType = parameter.tryGetType(); |
70 | var javaTransitiveInstancesKey = new JavaTransitiveInstancesKey(dataSort.type()); | 69 | if (parameterType.isPresent()) { |
71 | var javaImplication = new InputKeyImplication(implyingKey, javaTransitiveInstancesKey, | 70 | var javaTransitiveInstancesKey = new JavaTransitiveInstancesKey(parameterType.get()); |
72 | List.of(i)); | 71 | var javaImplication = new InputKeyImplication(implyingKey, javaTransitiveInstancesKey, List.of(i)); |
73 | inputKeyImplications.add(javaImplication); | 72 | inputKeyImplications.add(javaImplication); |
74 | } | 73 | } |
75 | } | 74 | } |
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 b511a5c7..ec880435 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 | |||
@@ -19,11 +19,13 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.Consta | |||
19 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall; | 19 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall; |
20 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint; | 20 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint; |
21 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter; | 21 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter; |
22 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameterDirection; | ||
22 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery; | 23 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery; |
23 | import org.eclipse.viatra.query.runtime.matchers.tuple.Tuple; | 24 | import org.eclipse.viatra.query.runtime.matchers.tuple.Tuple; |
24 | import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples; | 25 | import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples; |
25 | import tools.refinery.store.query.dnf.Dnf; | 26 | import tools.refinery.store.query.dnf.Dnf; |
26 | import tools.refinery.store.query.dnf.DnfClause; | 27 | import tools.refinery.store.query.dnf.DnfClause; |
28 | import tools.refinery.store.query.dnf.SymbolicParameter; | ||
27 | import tools.refinery.store.query.literal.*; | 29 | import tools.refinery.store.query.literal.*; |
28 | import tools.refinery.store.query.term.ConstantTerm; | 30 | import tools.refinery.store.query.term.ConstantTerm; |
29 | import tools.refinery.store.query.term.StatefulAggregator; | 31 | import tools.refinery.store.query.term.StatefulAggregator; |
@@ -82,15 +84,20 @@ public class Dnf2PQuery { | |||
82 | var pQuery = new RawPQuery(dnfQuery.getUniqueName()); | 84 | var pQuery = new RawPQuery(dnfQuery.getUniqueName()); |
83 | pQuery.setEvaluationHints(consumeHint(dnfQuery)); | 85 | pQuery.setEvaluationHints(consumeHint(dnfQuery)); |
84 | 86 | ||
85 | Map<Variable, PParameter> parameters = new HashMap<>(); | 87 | Map<SymbolicParameter, PParameter> parameters = new HashMap<>(); |
86 | for (Variable variable : dnfQuery.getParameters()) { | ||
87 | parameters.put(variable, new PParameter(variable.getUniqueName())); | ||
88 | } | ||
89 | |||
90 | List<PParameter> parameterList = new ArrayList<>(); | 88 | List<PParameter> parameterList = new ArrayList<>(); |
91 | for (var param : dnfQuery.getParameters()) { | 89 | for (var parameter : dnfQuery.getSymbolicParameters()) { |
92 | parameterList.add(parameters.get(param)); | 90 | var direction = switch (parameter.getDirection()) { |
91 | case IN_OUT -> PParameterDirection.INOUT; | ||
92 | case OUT -> PParameterDirection.OUT; | ||
93 | case IN -> throw new IllegalArgumentException("Query %s with input parameter %s is not supported" | ||
94 | .formatted(dnfQuery, parameter.getVariable())); | ||
95 | }; | ||
96 | var pParameter = new PParameter(parameter.getVariable().getUniqueName(), null, null, direction); | ||
97 | parameters.put(parameter, pParameter); | ||
98 | parameterList.add(pParameter); | ||
93 | } | 99 | } |
100 | |||
94 | pQuery.setParameters(parameterList); | 101 | pQuery.setParameters(parameterList); |
95 | 102 | ||
96 | for (var functionalDependency : dnfQuery.getFunctionalDependencies()) { | 103 | for (var functionalDependency : dnfQuery.getFunctionalDependencies()) { |
@@ -110,15 +117,15 @@ public class Dnf2PQuery { | |||
110 | synchronized (P_CONSTRAINT_LOCK) { | 117 | synchronized (P_CONSTRAINT_LOCK) { |
111 | for (DnfClause clause : dnfQuery.getClauses()) { | 118 | for (DnfClause clause : dnfQuery.getClauses()) { |
112 | PBody body = new PBody(pQuery); | 119 | PBody body = new PBody(pQuery); |
113 | List<ExportedParameter> symbolicParameters = new ArrayList<>(); | 120 | List<ExportedParameter> parameterExports = new ArrayList<>(); |
114 | for (var param : dnfQuery.getParameters()) { | 121 | for (var parameter : dnfQuery.getSymbolicParameters()) { |
115 | PVariable pVar = body.getOrCreateVariableByName(param.getUniqueName()); | 122 | PVariable pVar = body.getOrCreateVariableByName(parameter.getVariable().getUniqueName()); |
116 | symbolicParameters.add(new ExportedParameter(body, pVar, parameters.get(param))); | 123 | parameterExports.add(new ExportedParameter(body, pVar, parameters.get(parameter))); |
117 | } | 124 | } |
118 | body.setSymbolicParameters(symbolicParameters); | 125 | body.setSymbolicParameters(parameterExports); |
119 | pQuery.addBody(body); | 126 | pQuery.addBody(body); |
120 | for (Literal literal : clause.literals()) { | 127 | for (Literal literal : clause.literals()) { |
121 | translateLiteral(literal, clause, body); | 128 | translateLiteral(literal, body); |
122 | } | 129 | } |
123 | } | 130 | } |
124 | } | 131 | } |
@@ -126,11 +133,11 @@ public class Dnf2PQuery { | |||
126 | return pQuery; | 133 | return pQuery; |
127 | } | 134 | } |
128 | 135 | ||
129 | private void translateLiteral(Literal literal, DnfClause clause, PBody body) { | 136 | private void translateLiteral(Literal literal, PBody body) { |
130 | if (literal instanceof EquivalenceLiteral equivalenceLiteral) { | 137 | if (literal instanceof EquivalenceLiteral equivalenceLiteral) { |
131 | translateEquivalenceLiteral(equivalenceLiteral, body); | 138 | translateEquivalenceLiteral(equivalenceLiteral, body); |
132 | } else if (literal instanceof CallLiteral callLiteral) { | 139 | } else if (literal instanceof CallLiteral callLiteral) { |
133 | translateCallLiteral(callLiteral, clause, body); | 140 | translateCallLiteral(callLiteral, body); |
134 | } else if (literal instanceof ConstantLiteral constantLiteral) { | 141 | } else if (literal instanceof ConstantLiteral constantLiteral) { |
135 | translateConstantLiteral(constantLiteral, body); | 142 | translateConstantLiteral(constantLiteral, body); |
136 | } else if (literal instanceof AssignLiteral<?> assignLiteral) { | 143 | } else if (literal instanceof AssignLiteral<?> assignLiteral) { |
@@ -138,25 +145,25 @@ public class Dnf2PQuery { | |||
138 | } else if (literal instanceof AssumeLiteral assumeLiteral) { | 145 | } else if (literal instanceof AssumeLiteral assumeLiteral) { |
139 | translateAssumeLiteral(assumeLiteral, body); | 146 | translateAssumeLiteral(assumeLiteral, body); |
140 | } else if (literal instanceof CountLiteral countLiteral) { | 147 | } else if (literal instanceof CountLiteral countLiteral) { |
141 | translateCountLiteral(countLiteral, clause, body); | 148 | translateCountLiteral(countLiteral, body); |
142 | } else if (literal instanceof AggregationLiteral<?, ?> aggregationLiteral) { | 149 | } else if (literal instanceof AggregationLiteral<?, ?> aggregationLiteral) { |
143 | translateAggregationLiteral(aggregationLiteral, clause, body); | 150 | translateAggregationLiteral(aggregationLiteral, body); |
144 | } else { | 151 | } else { |
145 | throw new IllegalArgumentException("Unknown literal: " + literal.toString()); | 152 | throw new IllegalArgumentException("Unknown literal: " + literal.toString()); |
146 | } | 153 | } |
147 | } | 154 | } |
148 | 155 | ||
149 | private void translateEquivalenceLiteral(EquivalenceLiteral equivalenceLiteral, PBody body) { | 156 | private void translateEquivalenceLiteral(EquivalenceLiteral equivalenceLiteral, PBody body) { |
150 | PVariable varSource = body.getOrCreateVariableByName(equivalenceLiteral.left().getUniqueName()); | 157 | PVariable varSource = body.getOrCreateVariableByName(equivalenceLiteral.getLeft().getUniqueName()); |
151 | PVariable varTarget = body.getOrCreateVariableByName(equivalenceLiteral.right().getUniqueName()); | 158 | PVariable varTarget = body.getOrCreateVariableByName(equivalenceLiteral.getRight().getUniqueName()); |
152 | if (equivalenceLiteral.positive()) { | 159 | if (equivalenceLiteral.isPositive()) { |
153 | new Equality(body, varSource, varTarget); | 160 | new Equality(body, varSource, varTarget); |
154 | } else { | 161 | } else { |
155 | new Inequality(body, varSource, varTarget); | 162 | new Inequality(body, varSource, varTarget); |
156 | } | 163 | } |
157 | } | 164 | } |
158 | 165 | ||
159 | private void translateCallLiteral(CallLiteral callLiteral, DnfClause clause, PBody body) { | 166 | private void translateCallLiteral(CallLiteral callLiteral, PBody body) { |
160 | var polarity = callLiteral.getPolarity(); | 167 | var polarity = callLiteral.getPolarity(); |
161 | switch (polarity) { | 168 | switch (polarity) { |
162 | case POSITIVE -> { | 169 | case POSITIVE -> { |
@@ -186,7 +193,7 @@ public class Dnf2PQuery { | |||
186 | new BinaryTransitiveClosure(body, substitution, pattern); | 193 | new BinaryTransitiveClosure(body, substitution, pattern); |
187 | } | 194 | } |
188 | case NEGATIVE -> { | 195 | case NEGATIVE -> { |
189 | var wrappedCall = wrapperFactory.maybeWrapConstraint(callLiteral, clause); | 196 | var wrappedCall = wrapperFactory.maybeWrapConstraint(callLiteral); |
190 | var substitution = translateSubstitution(wrappedCall.remappedArguments(), body); | 197 | var substitution = translateSubstitution(wrappedCall.remappedArguments(), body); |
191 | var pattern = wrappedCall.pattern(); | 198 | var pattern = wrappedCall.pattern(); |
192 | new NegativePatternCall(body, substitution, pattern); | 199 | new NegativePatternCall(body, substitution, pattern); |
@@ -206,13 +213,13 @@ public class Dnf2PQuery { | |||
206 | } | 213 | } |
207 | 214 | ||
208 | private void translateConstantLiteral(ConstantLiteral constantLiteral, PBody body) { | 215 | private void translateConstantLiteral(ConstantLiteral constantLiteral, PBody body) { |
209 | var variable = body.getOrCreateVariableByName(constantLiteral.variable().getUniqueName()); | 216 | var variable = body.getOrCreateVariableByName(constantLiteral.getVariable().getUniqueName()); |
210 | new ConstantValue(body, variable, constantLiteral.nodeId()); | 217 | new ConstantValue(body, variable, constantLiteral.getNodeId()); |
211 | } | 218 | } |
212 | 219 | ||
213 | private <T> void translateAssignLiteral(AssignLiteral<T> assignLiteral, PBody body) { | 220 | private <T> void translateAssignLiteral(AssignLiteral<T> assignLiteral, PBody body) { |
214 | var variable = body.getOrCreateVariableByName(assignLiteral.variable().getUniqueName()); | 221 | var variable = body.getOrCreateVariableByName(assignLiteral.getTargetVariable().getUniqueName()); |
215 | var term = assignLiteral.term(); | 222 | var term = assignLiteral.getTerm(); |
216 | if (term instanceof ConstantTerm<T> constantTerm) { | 223 | if (term instanceof ConstantTerm<T> constantTerm) { |
217 | new ConstantValue(body, variable, constantTerm.getValue()); | 224 | new ConstantValue(body, variable, constantTerm.getValue()); |
218 | } else { | 225 | } else { |
@@ -222,19 +229,18 @@ public class Dnf2PQuery { | |||
222 | } | 229 | } |
223 | 230 | ||
224 | private void translateAssumeLiteral(AssumeLiteral assumeLiteral, PBody body) { | 231 | private void translateAssumeLiteral(AssumeLiteral assumeLiteral, PBody body) { |
225 | var evaluator = new AssumptionEvaluator(assumeLiteral.term()); | 232 | var evaluator = new AssumptionEvaluator(assumeLiteral.getTerm()); |
226 | new ExpressionEvaluation(body, evaluator, null); | 233 | new ExpressionEvaluation(body, evaluator, null); |
227 | } | 234 | } |
228 | 235 | ||
229 | private void translateCountLiteral(CountLiteral countLiteral, DnfClause clause, PBody body) { | 236 | private void translateCountLiteral(CountLiteral countLiteral, PBody body) { |
230 | var wrappedCall = wrapperFactory.maybeWrapConstraint(countLiteral, clause); | 237 | var wrappedCall = wrapperFactory.maybeWrapConstraint(countLiteral); |
231 | var substitution = translateSubstitution(wrappedCall.remappedArguments(), body); | 238 | var substitution = translateSubstitution(wrappedCall.remappedArguments(), body); |
232 | var resultVariable = body.getOrCreateVariableByName(countLiteral.getResultVariable().getUniqueName()); | 239 | var resultVariable = body.getOrCreateVariableByName(countLiteral.getResultVariable().getUniqueName()); |
233 | new PatternMatchCounter(body, substitution, wrappedCall.pattern(), resultVariable); | 240 | new PatternMatchCounter(body, substitution, wrappedCall.pattern(), resultVariable); |
234 | } | 241 | } |
235 | 242 | ||
236 | private <R, T> void translateAggregationLiteral(AggregationLiteral<R, T> aggregationLiteral, DnfClause clause, | 243 | private <R, T> void translateAggregationLiteral(AggregationLiteral<R, T> aggregationLiteral, PBody body) { |
237 | PBody body) { | ||
238 | var aggregator = aggregationLiteral.getAggregator(); | 244 | var aggregator = aggregationLiteral.getAggregator(); |
239 | IMultisetAggregationOperator<T, ?, R> aggregationOperator; | 245 | IMultisetAggregationOperator<T, ?, R> aggregationOperator; |
240 | if (aggregator instanceof StatelessAggregator<R, T> statelessAggregator) { | 246 | if (aggregator instanceof StatelessAggregator<R, T> statelessAggregator) { |
@@ -244,7 +250,7 @@ public class Dnf2PQuery { | |||
244 | } else { | 250 | } else { |
245 | throw new IllegalArgumentException("Unknown aggregator: " + aggregator); | 251 | throw new IllegalArgumentException("Unknown aggregator: " + aggregator); |
246 | } | 252 | } |
247 | var wrappedCall = wrapperFactory.maybeWrapConstraint(aggregationLiteral, clause); | 253 | var wrappedCall = wrapperFactory.maybeWrapConstraint(aggregationLiteral); |
248 | var substitution = translateSubstitution(wrappedCall.remappedArguments(), body); | 254 | var substitution = translateSubstitution(wrappedCall.remappedArguments(), body); |
249 | var inputVariable = body.getOrCreateVariableByName(aggregationLiteral.getInputVariable().getUniqueName()); | 255 | var inputVariable = body.getOrCreateVariableByName(aggregationLiteral.getInputVariable().getUniqueName()); |
250 | var aggregatedColumn = substitution.invertIndex().get(inputVariable); | 256 | var aggregatedColumn = substitution.invertIndex().get(inputVariable); |
diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/QueryWrapperFactory.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/QueryWrapperFactory.java index 0d046455..2b7280f2 100644 --- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/QueryWrapperFactory.java +++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/QueryWrapperFactory.java | |||
@@ -14,12 +14,13 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeCo | |||
14 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter; | 14 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter; |
15 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery; | 15 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery; |
16 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PVisibility; | 16 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PVisibility; |
17 | import org.eclipse.viatra.query.runtime.matchers.tuple.Tuple; | ||
17 | import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples; | 18 | import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples; |
18 | import tools.refinery.store.query.Constraint; | 19 | import tools.refinery.store.query.Constraint; |
19 | import tools.refinery.store.query.dnf.Dnf; | 20 | import tools.refinery.store.query.dnf.Dnf; |
20 | import tools.refinery.store.query.dnf.DnfClause; | ||
21 | import tools.refinery.store.query.dnf.DnfUtils; | 21 | import tools.refinery.store.query.dnf.DnfUtils; |
22 | import tools.refinery.store.query.literal.AbstractCallLiteral; | 22 | import tools.refinery.store.query.literal.AbstractCallLiteral; |
23 | import tools.refinery.store.query.term.ParameterDirection; | ||
23 | import tools.refinery.store.query.term.Variable; | 24 | import tools.refinery.store.query.term.Variable; |
24 | import tools.refinery.store.query.view.AnySymbolView; | 25 | import tools.refinery.store.query.view.AnySymbolView; |
25 | import tools.refinery.store.query.view.SymbolView; | 26 | import tools.refinery.store.query.view.SymbolView; |
@@ -45,21 +46,17 @@ class QueryWrapperFactory { | |||
45 | } | 46 | } |
46 | return maybeWrapConstraint(symbolView, identity); | 47 | return maybeWrapConstraint(symbolView, identity); |
47 | } | 48 | } |
48 | public WrappedCall maybeWrapConstraint(AbstractCallLiteral callLiteral, DnfClause clause) { | 49 | |
50 | public WrappedCall maybeWrapConstraint(AbstractCallLiteral callLiteral) { | ||
49 | var arguments = callLiteral.getArguments(); | 51 | var arguments = callLiteral.getArguments(); |
50 | int arity = arguments.size(); | 52 | int arity = arguments.size(); |
51 | var remappedParameters = new int[arity]; | 53 | var remappedParameters = new int[arity]; |
52 | var boundVariables = clause.boundVariables(); | ||
53 | var unboundVariableIndices = new HashMap<Variable, Integer>(); | 54 | var unboundVariableIndices = new HashMap<Variable, Integer>(); |
54 | var appendVariable = new VariableAppender(); | 55 | var appendVariable = new VariableAppender(); |
55 | for (int i = 0; i < arity; i++) { | 56 | for (int i = 0; i < arity; i++) { |
56 | var variable = arguments.get(i); | 57 | var variable = arguments.get(i); |
57 | if (boundVariables.contains(variable)) { | 58 | // Unify all variables to avoid VIATRA bugs, even if they're bound in the containing clause. |
58 | // Do not join bound variable to make sure that the embedded pattern stays as general as possible. | 59 | remappedParameters[i] = unboundVariableIndices.computeIfAbsent(variable, appendVariable::applyAsInt); |
59 | remappedParameters[i] = appendVariable.applyAsInt(variable); | ||
60 | } else { | ||
61 | remappedParameters[i] = unboundVariableIndices.computeIfAbsent(variable, appendVariable::applyAsInt); | ||
62 | } | ||
63 | } | 60 | } |
64 | var pattern = maybeWrapConstraint(callLiteral.getTarget(), remappedParameters); | 61 | var pattern = maybeWrapConstraint(callLiteral.getTarget(), remappedParameters); |
65 | return new WrappedCall(pattern, appendVariable.getRemappedArguments()); | 62 | return new WrappedCall(pattern, appendVariable.getRemappedArguments()); |
@@ -89,6 +86,8 @@ class QueryWrapperFactory { | |||
89 | var constraint = remappedConstraint.constraint(); | 86 | var constraint = remappedConstraint.constraint(); |
90 | var remappedParameters = remappedConstraint.remappedParameters(); | 87 | var remappedParameters = remappedConstraint.remappedParameters(); |
91 | 88 | ||
89 | checkNoInputParameters(constraint); | ||
90 | |||
92 | var embeddedPQuery = new RawPQuery(DnfUtils.generateUniqueName(constraint.name()), PVisibility.EMBEDDED); | 91 | var embeddedPQuery = new RawPQuery(DnfUtils.generateUniqueName(constraint.name()), PVisibility.EMBEDDED); |
93 | var body = new PBody(embeddedPQuery); | 92 | var body = new PBody(embeddedPQuery); |
94 | int arity = Arrays.stream(remappedParameters).max().orElse(-1) + 1; | 93 | int arity = Arrays.stream(remappedParameters).max().orElse(-1) + 1; |
@@ -112,6 +111,21 @@ class QueryWrapperFactory { | |||
112 | } | 111 | } |
113 | var argumentTuple = Tuples.flatTupleOf(arguments); | 112 | var argumentTuple = Tuples.flatTupleOf(arguments); |
114 | 113 | ||
114 | addPositiveConstraint(constraint, body, argumentTuple); | ||
115 | embeddedPQuery.addBody(body); | ||
116 | return embeddedPQuery; | ||
117 | } | ||
118 | |||
119 | private static void checkNoInputParameters(Constraint constraint) { | ||
120 | for (var constraintParameter : constraint.getParameters()) { | ||
121 | if (constraintParameter.getDirection() == ParameterDirection.IN) { | ||
122 | throw new IllegalArgumentException("Input parameter %s of %s is not supported" | ||
123 | .formatted(constraintParameter, constraint)); | ||
124 | } | ||
125 | } | ||
126 | } | ||
127 | |||
128 | private void addPositiveConstraint(Constraint constraint, PBody body, Tuple argumentTuple) { | ||
115 | if (constraint instanceof SymbolView<?> view) { | 129 | if (constraint instanceof SymbolView<?> view) { |
116 | new TypeConstraint(body, argumentTuple, getInputKey(view)); | 130 | new TypeConstraint(body, argumentTuple, getInputKey(view)); |
117 | } else if (constraint instanceof Dnf dnf) { | 131 | } else if (constraint instanceof Dnf dnf) { |
@@ -120,9 +134,6 @@ class QueryWrapperFactory { | |||
120 | } else { | 134 | } else { |
121 | throw new IllegalArgumentException("Unknown Constraint: " + constraint); | 135 | throw new IllegalArgumentException("Unknown Constraint: " + constraint); |
122 | } | 136 | } |
123 | |||
124 | embeddedPQuery.addBody(body); | ||
125 | return embeddedPQuery; | ||
126 | } | 137 | } |
127 | 138 | ||
128 | public IInputKey getInputKey(AnySymbolView symbolView) { | 139 | public IInputKey getInputKey(AnySymbolView symbolView) { |
diff --git a/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/DiagonalQueryTest.java b/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/DiagonalQueryTest.java index 56ddb9b4..86a27f5b 100644 --- a/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/DiagonalQueryTest.java +++ b/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/DiagonalQueryTest.java | |||
@@ -298,10 +298,10 @@ class DiagonalQueryTest { | |||
298 | y.assign(x) | 298 | y.assign(x) |
299 | ); | 299 | ); |
300 | }); | 300 | }); |
301 | var query = Query.of("Diagonal", Integer.class, (builder, p1, output) -> builder.clause(Integer.class, | 301 | var query = Query.of("Diagonal", Integer.class, (builder, p1, output) -> builder.clause( |
302 | (p2, y) -> List.of( | 302 | Integer.class, Integer.class, (p2, y, z) -> List.of( |
303 | personView.call(p1), | 303 | personView.call(p1), |
304 | output.assign(subQuery.aggregate(y, INT_SUM, p1, p1, p2, p2, y, y)) | 304 | output.assign(subQuery.aggregate(y, INT_SUM, p1, p1, p2, p2, y, z)) |
305 | ))); | 305 | ))); |
306 | 306 | ||
307 | var store = ModelStore.builder() | 307 | var store = ModelStore.builder() |
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 10d8a579..207c627c 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 | |||
@@ -14,10 +14,10 @@ import java.util.List; | |||
14 | public interface Constraint { | 14 | public interface Constraint { |
15 | String name(); | 15 | String name(); |
16 | 16 | ||
17 | List<Sort> getSorts(); | 17 | List<Parameter> getParameters(); |
18 | 18 | ||
19 | default int arity() { | 19 | default int arity() { |
20 | return getSorts().size(); | 20 | return getParameters().size(); |
21 | } | 21 | } |
22 | 22 | ||
23 | default boolean invalidIndex(int i) { | 23 | default boolean invalidIndex(int i) { |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/AbstractQueryBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/AbstractQueryBuilder.java index ddd69b9f..2a3e3ce0 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/AbstractQueryBuilder.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/AbstractQueryBuilder.java | |||
@@ -8,6 +8,7 @@ package tools.refinery.store.query.dnf; | |||
8 | import tools.refinery.store.query.dnf.callback.*; | 8 | import tools.refinery.store.query.dnf.callback.*; |
9 | import tools.refinery.store.query.literal.Literal; | 9 | import tools.refinery.store.query.literal.Literal; |
10 | import tools.refinery.store.query.term.NodeVariable; | 10 | import tools.refinery.store.query.term.NodeVariable; |
11 | import tools.refinery.store.query.term.ParameterDirection; | ||
11 | import tools.refinery.store.query.term.Variable; | 12 | import tools.refinery.store.query.term.Variable; |
12 | 13 | ||
13 | import java.util.Collection; | 14 | import java.util.Collection; |
@@ -31,11 +32,24 @@ public abstract class AbstractQueryBuilder<T extends AbstractQueryBuilder<T>> { | |||
31 | return dnfBuilder.parameter(name); | 32 | return dnfBuilder.parameter(name); |
32 | } | 33 | } |
33 | 34 | ||
35 | public NodeVariable parameter(ParameterDirection direction) { | ||
36 | return dnfBuilder.parameter(direction); | ||
37 | } | ||
38 | |||
39 | public NodeVariable parameter(String name, ParameterDirection direction) { | ||
40 | return dnfBuilder.parameter(name, direction); | ||
41 | } | ||
42 | |||
34 | public T parameter(NodeVariable variable) { | 43 | public T parameter(NodeVariable variable) { |
35 | dnfBuilder.parameter(variable); | 44 | dnfBuilder.parameter(variable); |
36 | return self(); | 45 | return self(); |
37 | } | 46 | } |
38 | 47 | ||
48 | public T parameter(NodeVariable variable, ParameterDirection direction) { | ||
49 | dnfBuilder.parameter(variable, direction); | ||
50 | return self(); | ||
51 | } | ||
52 | |||
39 | public T parameters(NodeVariable... variables) { | 53 | public T parameters(NodeVariable... variables) { |
40 | dnfBuilder.parameters(variables); | 54 | dnfBuilder.parameters(variables); |
41 | return self(); | 55 | return self(); |
@@ -46,6 +60,16 @@ public abstract class AbstractQueryBuilder<T extends AbstractQueryBuilder<T>> { | |||
46 | return self(); | 60 | return self(); |
47 | } | 61 | } |
48 | 62 | ||
63 | public T parameters(List<NodeVariable> variables, ParameterDirection direction) { | ||
64 | dnfBuilder.parameters(variables, direction); | ||
65 | return self(); | ||
66 | } | ||
67 | |||
68 | public T symbolicParameters(List<SymbolicParameter> parameters) { | ||
69 | dnfBuilder.symbolicParameters(parameters); | ||
70 | return self(); | ||
71 | } | ||
72 | |||
49 | public T functionalDependencies(Collection<FunctionalDependency<Variable>> functionalDependencies) { | 73 | public T functionalDependencies(Collection<FunctionalDependency<Variable>> functionalDependencies) { |
50 | dnfBuilder.functionalDependencies(functionalDependencies); | 74 | dnfBuilder.functionalDependencies(functionalDependencies); |
51 | return self(); | 75 | return self(); |
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 new file mode 100644 index 00000000..7a56145c --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java | |||
@@ -0,0 +1,321 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.query.dnf; | ||
7 | |||
8 | import org.jetbrains.annotations.NotNull; | ||
9 | import tools.refinery.store.query.literal.EquivalenceLiteral; | ||
10 | import tools.refinery.store.query.literal.Literal; | ||
11 | import tools.refinery.store.query.literal.VariableDirection; | ||
12 | import tools.refinery.store.query.substitution.MapBasedSubstitution; | ||
13 | import tools.refinery.store.query.substitution.StatelessSubstitution; | ||
14 | import tools.refinery.store.query.term.NodeVariable; | ||
15 | import tools.refinery.store.query.term.Variable; | ||
16 | |||
17 | import java.util.*; | ||
18 | import java.util.function.Function; | ||
19 | import java.util.stream.Collectors; | ||
20 | |||
21 | class ClausePostProcessor { | ||
22 | private final Set<Variable> parameters; | ||
23 | private final Map<Variable, Integer> parameterWeights; | ||
24 | private final List<Literal> literals; | ||
25 | private final Map<NodeVariable, NodeVariable> representatives = new LinkedHashMap<>(); | ||
26 | private final Map<NodeVariable, Set<NodeVariable>> equivalencePartition = new HashMap<>(); | ||
27 | private List<Literal> substitutedLiterals; | ||
28 | private final Set<Variable> existentiallyQuantifiedVariables = new LinkedHashSet<>(); | ||
29 | private Set<Variable> inputParameters; | ||
30 | private Set<Variable> positiveVariables; | ||
31 | private Map<Variable, Set<SortableLiteral>> variableToLiteralInputMap; | ||
32 | private PriorityQueue<SortableLiteral> literalsWithAllInputsBound; | ||
33 | private LinkedHashSet<Literal> topologicallySortedLiterals; | ||
34 | |||
35 | public ClausePostProcessor(Set<Variable> parameters, Map<Variable, Integer> parameterWeights, | ||
36 | List<Literal> literals) { | ||
37 | this.parameters = parameters; | ||
38 | this.parameterWeights = parameterWeights; | ||
39 | this.literals = literals; | ||
40 | } | ||
41 | |||
42 | public Result postProcessClause() { | ||
43 | mergeEquivalentNodeVariables(); | ||
44 | substitutedLiterals = new ArrayList<>(literals.size()); | ||
45 | keepParameterEquivalences(); | ||
46 | substituteLiterals(); | ||
47 | computePositiveVariables(); | ||
48 | validatePositiveRepresentatives(); | ||
49 | validateClosureVariables(); | ||
50 | topologicallySortLiterals(); | ||
51 | var filteredLiterals = new ArrayList<Literal>(topologicallySortedLiterals.size()); | ||
52 | for (var literal : topologicallySortedLiterals) { | ||
53 | var reduction = literal.getReduction(); | ||
54 | switch (reduction) { | ||
55 | case NOT_REDUCIBLE -> filteredLiterals.add(literal); | ||
56 | case ALWAYS_TRUE -> { | ||
57 | // Literals reducible to {@code true} can be omitted, because the model is always assumed to have at | ||
58 | // least on object. | ||
59 | } | ||
60 | case ALWAYS_FALSE -> { | ||
61 | // Clauses with {@code false} literals can be omitted entirely. | ||
62 | return ConstantResult.ALWAYS_FALSE; | ||
63 | } | ||
64 | default -> throw new IllegalArgumentException("Invalid reduction: " + reduction); | ||
65 | } | ||
66 | } | ||
67 | if (filteredLiterals.isEmpty()) { | ||
68 | return ConstantResult.ALWAYS_TRUE; | ||
69 | } | ||
70 | var clause = new DnfClause(Collections.unmodifiableSet(positiveVariables), | ||
71 | Collections.unmodifiableList(filteredLiterals)); | ||
72 | return new ClauseResult(clause); | ||
73 | } | ||
74 | |||
75 | private void mergeEquivalentNodeVariables() { | ||
76 | for (var literal : literals) { | ||
77 | if (isPositiveEquivalence(literal)) { | ||
78 | var equivalenceLiteral = (EquivalenceLiteral) literal; | ||
79 | mergeVariables(equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); | ||
80 | } | ||
81 | } | ||
82 | } | ||
83 | |||
84 | private static boolean isPositiveEquivalence(Literal literal) { | ||
85 | return literal instanceof EquivalenceLiteral equivalenceLiteral && equivalenceLiteral.isPositive(); | ||
86 | } | ||
87 | |||
88 | private void mergeVariables(NodeVariable left, NodeVariable right) { | ||
89 | var leftRepresentative = getRepresentative(left); | ||
90 | var rightRepresentative = getRepresentative(right); | ||
91 | if (parameters.contains(leftRepresentative) && (!parameters.contains(rightRepresentative) || | ||
92 | parameterWeights.get(leftRepresentative).compareTo(parameterWeights.get(rightRepresentative)) <= 0)) { | ||
93 | // Prefer the variable occurring earlier in the parameter list as a representative. | ||
94 | doMergeVariables(leftRepresentative, rightRepresentative); | ||
95 | } else { | ||
96 | doMergeVariables(rightRepresentative, leftRepresentative); | ||
97 | } | ||
98 | } | ||
99 | |||
100 | private void doMergeVariables(NodeVariable parentRepresentative, NodeVariable newChildRepresentative) { | ||
101 | var parentSet = getEquivalentVariables(parentRepresentative); | ||
102 | var childSet = getEquivalentVariables(newChildRepresentative); | ||
103 | parentSet.addAll(childSet); | ||
104 | equivalencePartition.remove(newChildRepresentative); | ||
105 | for (var childEquivalentNodeVariable : childSet) { | ||
106 | representatives.put(childEquivalentNodeVariable, parentRepresentative); | ||
107 | } | ||
108 | } | ||
109 | |||
110 | private NodeVariable getRepresentative(NodeVariable variable) { | ||
111 | return representatives.computeIfAbsent(variable, Function.identity()); | ||
112 | } | ||
113 | |||
114 | private Set<NodeVariable> getEquivalentVariables(NodeVariable variable) { | ||
115 | var representative = getRepresentative(variable); | ||
116 | if (!representative.equals(variable)) { | ||
117 | throw new IllegalStateException("NodeVariable %s already has a representative %s" | ||
118 | .formatted(variable, representative)); | ||
119 | } | ||
120 | return equivalencePartition.computeIfAbsent(variable, key -> { | ||
121 | var set = new HashSet<NodeVariable>(1); | ||
122 | set.add(key); | ||
123 | return set; | ||
124 | }); | ||
125 | } | ||
126 | |||
127 | private void keepParameterEquivalences() { | ||
128 | for (var pair : representatives.entrySet()) { | ||
129 | var left = pair.getKey(); | ||
130 | var right = pair.getValue(); | ||
131 | if (!left.equals(right) && parameters.contains(left) && parameters.contains(right)) { | ||
132 | substitutedLiterals.add(left.isEquivalent(right)); | ||
133 | } | ||
134 | } | ||
135 | } | ||
136 | |||
137 | private void substituteLiterals() { | ||
138 | var substitution = new MapBasedSubstitution(Collections.unmodifiableMap(representatives), | ||
139 | StatelessSubstitution.IDENTITY); | ||
140 | for (var literal : literals) { | ||
141 | if (isPositiveEquivalence(literal)) { | ||
142 | // We already retained all equivalences that cannot be replaced with substitutions in | ||
143 | // {@link#keepParameterEquivalences()}. | ||
144 | continue; | ||
145 | } | ||
146 | var substitutedLiteral = literal.substitute(substitution); | ||
147 | substitutedLiterals.add(substitutedLiteral); | ||
148 | } | ||
149 | } | ||
150 | |||
151 | private void computePositiveVariables() { | ||
152 | for (var literal : substitutedLiterals) { | ||
153 | var variableBinder = literal.getVariableBinder(); | ||
154 | variableBinder.getVariablesWithDirection(VariableDirection.IN_OUT) | ||
155 | .forEach(existentiallyQuantifiedVariables::add); | ||
156 | variableBinder.getVariablesWithDirection(VariableDirection.OUT).forEach(variable -> { | ||
157 | boolean added = existentiallyQuantifiedVariables.add(variable); | ||
158 | if (!added) { | ||
159 | throw new IllegalArgumentException("Variable %s has multiple %s bindings" | ||
160 | .formatted(variable, VariableDirection.OUT)); | ||
161 | } | ||
162 | }); | ||
163 | } | ||
164 | // Input parameters are parameters not bound by any positive literal. | ||
165 | inputParameters = new LinkedHashSet<>(parameters); | ||
166 | inputParameters.removeAll(existentiallyQuantifiedVariables); | ||
167 | // Existentially quantified variables are variables appearing in positive literals that aren't parameters. | ||
168 | existentiallyQuantifiedVariables.removeAll(parameters); | ||
169 | // Positive variables are parameters (including input parameters) and variables bound by positive literals. | ||
170 | positiveVariables = new LinkedHashSet<>(parameters.size() + existentiallyQuantifiedVariables.size()); | ||
171 | positiveVariables.addAll(parameters); | ||
172 | positiveVariables.addAll(existentiallyQuantifiedVariables); | ||
173 | } | ||
174 | |||
175 | private void validatePositiveRepresentatives() { | ||
176 | for (var pair : equivalencePartition.entrySet()) { | ||
177 | var representative = pair.getKey(); | ||
178 | if (!positiveVariables.contains(representative)) { | ||
179 | var variableSet = pair.getValue(); | ||
180 | throw new IllegalArgumentException("Variables %s were merged by equivalence but are not bound" | ||
181 | .formatted(variableSet)); | ||
182 | } | ||
183 | } | ||
184 | } | ||
185 | |||
186 | private void validateClosureVariables() { | ||
187 | var negativeVariablesMap = new HashMap<Variable, Literal>(); | ||
188 | for (var literal : substitutedLiterals) { | ||
189 | var variableBinder = literal.getVariableBinder(); | ||
190 | variableBinder.getVariablesWithDirection(VariableDirection.CLOSURE, positiveVariables) | ||
191 | .forEach(variable -> { | ||
192 | var oldLiteral = negativeVariablesMap.put(variable, literal); | ||
193 | if (oldLiteral != null) { | ||
194 | throw new IllegalArgumentException( | ||
195 | "Unbound variable %s appears in multiple literals %s and %s" | ||
196 | .formatted(variable, oldLiteral, literal)); | ||
197 | } | ||
198 | }); | ||
199 | } | ||
200 | } | ||
201 | |||
202 | private void topologicallySortLiterals() { | ||
203 | topologicallySortedLiterals = new LinkedHashSet<>(substitutedLiterals.size()); | ||
204 | variableToLiteralInputMap = new HashMap<>(); | ||
205 | literalsWithAllInputsBound = new PriorityQueue<>(); | ||
206 | int size = substitutedLiterals.size(); | ||
207 | for (int i = 0; i < size; i++) { | ||
208 | var literal = substitutedLiterals.get(i); | ||
209 | var sortableLiteral = new SortableLiteral(i, literal); | ||
210 | sortableLiteral.enqueue(); | ||
211 | } | ||
212 | while (!literalsWithAllInputsBound.isEmpty()) { | ||
213 | var variable = literalsWithAllInputsBound.remove(); | ||
214 | variable.addToSortedLiterals(); | ||
215 | } | ||
216 | if (!variableToLiteralInputMap.isEmpty()) { | ||
217 | throw new IllegalArgumentException("Unbound input variables %s" | ||
218 | .formatted(variableToLiteralInputMap.keySet())); | ||
219 | } | ||
220 | } | ||
221 | |||
222 | private void topologicallySortVariable(Variable variable) { | ||
223 | var literalSetForInput = variableToLiteralInputMap.remove(variable); | ||
224 | if (literalSetForInput == null) { | ||
225 | return; | ||
226 | } | ||
227 | for (var targetSortableLiteral : literalSetForInput) { | ||
228 | targetSortableLiteral.bindVariable(variable); | ||
229 | } | ||
230 | } | ||
231 | |||
232 | private class SortableLiteral implements Comparable<SortableLiteral> { | ||
233 | private final int index; | ||
234 | private final Literal literal; | ||
235 | private final Set<Variable> remainingInputs; | ||
236 | |||
237 | private SortableLiteral(int index, Literal literal) { | ||
238 | this.index = index; | ||
239 | this.literal = literal; | ||
240 | remainingInputs = literal.getVariableBinder() | ||
241 | .getVariablesWithDirection(VariableDirection.IN, positiveVariables) | ||
242 | .collect(Collectors.toCollection(HashSet::new)); | ||
243 | remainingInputs.removeAll(inputParameters); | ||
244 | } | ||
245 | |||
246 | public void enqueue() { | ||
247 | if (allInputsBound()) { | ||
248 | addToAllInputsBoundQueue(); | ||
249 | } else { | ||
250 | addToVariableToLiteralInputMap(); | ||
251 | } | ||
252 | } | ||
253 | |||
254 | private void bindVariable(Variable input) { | ||
255 | if (!remainingInputs.remove(input)) { | ||
256 | throw new IllegalStateException("Already processed input %s of literal %s".formatted(input, literal)); | ||
257 | } | ||
258 | if (allInputsBound()) { | ||
259 | addToAllInputsBoundQueue(); | ||
260 | } | ||
261 | } | ||
262 | |||
263 | private boolean allInputsBound() { | ||
264 | return remainingInputs.isEmpty(); | ||
265 | } | ||
266 | |||
267 | private void addToVariableToLiteralInputMap() { | ||
268 | for (var inputVariable : remainingInputs) { | ||
269 | var literalSetForInput = variableToLiteralInputMap.computeIfAbsent( | ||
270 | inputVariable, key -> new HashSet<>()); | ||
271 | literalSetForInput.add(this); | ||
272 | } | ||
273 | } | ||
274 | |||
275 | private void addToAllInputsBoundQueue() { | ||
276 | literalsWithAllInputsBound.add(this); | ||
277 | } | ||
278 | |||
279 | public void addToSortedLiterals() { | ||
280 | if (!allInputsBound()) { | ||
281 | throw new AssertionError("Inputs %s of %s are not yet bound".formatted(remainingInputs, literal)); | ||
282 | } | ||
283 | // Add literal if we haven't yet added a duplicate of this literal. | ||
284 | topologicallySortedLiterals.add(literal); | ||
285 | var variableBinder = literal.getVariableBinder(); | ||
286 | variableBinder.getVariablesWithDirection(VariableDirection.IN_OUT) | ||
287 | .forEach(ClausePostProcessor.this::topologicallySortVariable); | ||
288 | variableBinder.getVariablesWithDirection(VariableDirection.OUT) | ||
289 | .forEach(ClausePostProcessor.this::topologicallySortVariable); | ||
290 | } | ||
291 | |||
292 | @Override | ||
293 | public int compareTo(@NotNull ClausePostProcessor.SortableLiteral other) { | ||
294 | return Integer.compare(index, other.index); | ||
295 | } | ||
296 | |||
297 | @Override | ||
298 | public boolean equals(Object o) { | ||
299 | if (this == o) return true; | ||
300 | if (o == null || getClass() != o.getClass()) return false; | ||
301 | SortableLiteral that = (SortableLiteral) o; | ||
302 | return index == that.index && Objects.equals(literal, that.literal); | ||
303 | } | ||
304 | |||
305 | @Override | ||
306 | public int hashCode() { | ||
307 | return Objects.hash(index, literal); | ||
308 | } | ||
309 | } | ||
310 | |||
311 | public sealed interface Result permits ClauseResult, ConstantResult { | ||
312 | } | ||
313 | |||
314 | public record ClauseResult(DnfClause clause) implements Result { | ||
315 | } | ||
316 | |||
317 | public enum ConstantResult implements Result { | ||
318 | ALWAYS_TRUE, | ||
319 | ALWAYS_FALSE | ||
320 | } | ||
321 | } | ||
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 8de5079d..7e68d4a0 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 | |||
@@ -5,59 +5,57 @@ | |||
5 | */ | 5 | */ |
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.equality.DnfEqualityChecker; | 9 | import tools.refinery.store.query.equality.DnfEqualityChecker; |
9 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | 10 | import tools.refinery.store.query.equality.LiteralEqualityHelper; |
10 | import tools.refinery.store.query.Constraint; | ||
11 | import tools.refinery.store.query.literal.LiteralReduction; | 11 | import tools.refinery.store.query.literal.LiteralReduction; |
12 | import tools.refinery.store.query.term.Sort; | 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 | ||
15 | import java.util.Collection; | 15 | import java.util.Collection; |
16 | import java.util.HashSet; | 16 | import java.util.Collections; |
17 | import java.util.List; | 17 | import java.util.List; |
18 | import java.util.Set; | 18 | import java.util.Set; |
19 | import java.util.function.Consumer; | 19 | import java.util.function.Consumer; |
20 | import java.util.stream.Collectors; | ||
20 | 21 | ||
21 | public final class Dnf implements Constraint { | 22 | public final class Dnf implements Constraint { |
22 | private static final String INDENTATION = " "; | 23 | private static final String INDENTATION = " "; |
23 | 24 | ||
24 | private final String name; | 25 | private final String name; |
25 | |||
26 | private final String uniqueName; | 26 | private final String uniqueName; |
27 | 27 | private final List<SymbolicParameter> symbolicParameters; | |
28 | private final List<Variable> parameters; | ||
29 | |||
30 | private final List<FunctionalDependency<Variable>> functionalDependencies; | 28 | private final List<FunctionalDependency<Variable>> functionalDependencies; |
31 | |||
32 | private final List<DnfClause> clauses; | 29 | private final List<DnfClause> clauses; |
33 | 30 | ||
34 | Dnf(String name, List<Variable> parameters, List<FunctionalDependency<Variable>> functionalDependencies, | 31 | Dnf(String name, List<SymbolicParameter> symbolicParameters, |
35 | List<DnfClause> clauses) { | 32 | List<FunctionalDependency<Variable>> functionalDependencies, List<DnfClause> clauses) { |
36 | validateFunctionalDependencies(parameters, functionalDependencies); | 33 | validateFunctionalDependencies(symbolicParameters, functionalDependencies); |
37 | this.name = name; | 34 | this.name = name; |
38 | this.uniqueName = DnfUtils.generateUniqueName(name); | 35 | this.uniqueName = DnfUtils.generateUniqueName(name); |
39 | this.parameters = parameters; | 36 | this.symbolicParameters = symbolicParameters; |
40 | this.functionalDependencies = functionalDependencies; | 37 | this.functionalDependencies = functionalDependencies; |
41 | this.clauses = clauses; | 38 | this.clauses = clauses; |
42 | } | 39 | } |
43 | 40 | ||
44 | private static void validateFunctionalDependencies( | 41 | private static void validateFunctionalDependencies( |
45 | Collection<Variable> parameters, Collection<FunctionalDependency<Variable>> functionalDependencies) { | 42 | Collection<SymbolicParameter> symbolicParameters, |
46 | var parameterSet = new HashSet<>(parameters); | 43 | Collection<FunctionalDependency<Variable>> functionalDependencies) { |
44 | var parameterSet = symbolicParameters.stream().map(SymbolicParameter::getVariable).collect(Collectors.toSet()); | ||
47 | for (var functionalDependency : functionalDependencies) { | 45 | for (var functionalDependency : functionalDependencies) { |
48 | validateParameters(parameters, parameterSet, functionalDependency.forEach(), functionalDependency); | 46 | validateParameters(symbolicParameters, parameterSet, functionalDependency.forEach(), functionalDependency); |
49 | validateParameters(parameters, parameterSet, functionalDependency.unique(), functionalDependency); | 47 | validateParameters(symbolicParameters, parameterSet, functionalDependency.unique(), functionalDependency); |
50 | } | 48 | } |
51 | } | 49 | } |
52 | 50 | ||
53 | private static void validateParameters(Collection<Variable> parameters, Set<Variable> parameterSet, | 51 | private static void validateParameters(Collection<SymbolicParameter> symbolicParameters, |
54 | Collection<Variable> toValidate, | 52 | Set<Variable> parameterSet, Collection<Variable> toValidate, |
55 | FunctionalDependency<Variable> functionalDependency) { | 53 | FunctionalDependency<Variable> functionalDependency) { |
56 | for (var variable : toValidate) { | 54 | for (var variable : toValidate) { |
57 | if (!parameterSet.contains(variable)) { | 55 | if (!parameterSet.contains(variable)) { |
58 | throw new IllegalArgumentException( | 56 | throw new IllegalArgumentException( |
59 | "Variable %s of functional dependency %s does not appear in the parameter list %s" | 57 | "Variable %s of functional dependency %s does not appear in the parameter list %s" |
60 | .formatted(variable, functionalDependency, parameters)); | 58 | .formatted(variable, functionalDependency, symbolicParameters)); |
61 | } | 59 | } |
62 | } | 60 | } |
63 | } | 61 | } |
@@ -75,13 +73,12 @@ public final class Dnf implements Constraint { | |||
75 | return uniqueName; | 73 | return uniqueName; |
76 | } | 74 | } |
77 | 75 | ||
78 | public List<Variable> getParameters() { | 76 | public List<SymbolicParameter> getSymbolicParameters() { |
79 | return parameters; | 77 | return symbolicParameters; |
80 | } | 78 | } |
81 | 79 | ||
82 | @Override | 80 | public List<Parameter> getParameters() { |
83 | public List<Sort> getSorts() { | 81 | return Collections.unmodifiableList(symbolicParameters); |
84 | return parameters.stream().map(Variable::getSort).toList(); | ||
85 | } | 82 | } |
86 | 83 | ||
87 | public List<FunctionalDependency<Variable>> getFunctionalDependencies() { | 84 | public List<FunctionalDependency<Variable>> getFunctionalDependencies() { |
@@ -90,7 +87,7 @@ public final class Dnf implements Constraint { | |||
90 | 87 | ||
91 | @Override | 88 | @Override |
92 | public int arity() { | 89 | public int arity() { |
93 | return parameters.size(); | 90 | return symbolicParameters.size(); |
94 | } | 91 | } |
95 | 92 | ||
96 | public List<DnfClause> getClauses() { | 93 | public List<DnfClause> getClauses() { |
@@ -127,7 +124,8 @@ public final class Dnf implements Constraint { | |||
127 | return false; | 124 | return false; |
128 | } | 125 | } |
129 | for (int i = 0; i < numClauses; i++) { | 126 | for (int i = 0; i < numClauses; i++) { |
130 | var literalEqualityHelper = new LiteralEqualityHelper(callEqualityChecker, parameters, other.parameters); | 127 | var literalEqualityHelper = new LiteralEqualityHelper(callEqualityChecker, symbolicParameters, |
128 | other.symbolicParameters); | ||
131 | if (!clauses.get(i).equalsWithSubstitution(literalEqualityHelper, other.clauses.get(i))) { | 129 | if (!clauses.get(i).equalsWithSubstitution(literalEqualityHelper, other.clauses.get(i))) { |
132 | return false; | 130 | return false; |
133 | } | 131 | } |
@@ -145,18 +143,18 @@ public final class Dnf implements Constraint { | |||
145 | 143 | ||
146 | @Override | 144 | @Override |
147 | public String toString() { | 145 | public String toString() { |
148 | return "%s/%d".formatted(name, arity()); | 146 | return "%s/%d".formatted(name(), arity()); |
149 | } | 147 | } |
150 | 148 | ||
151 | @Override | 149 | @Override |
152 | public String toReferenceString() { | 150 | public String toReferenceString() { |
153 | return "@Dnf " + name; | 151 | return "@Dnf " + name(); |
154 | } | 152 | } |
155 | 153 | ||
156 | public String toDefinitionString() { | 154 | public String toDefinitionString() { |
157 | var builder = new StringBuilder(); | 155 | var builder = new StringBuilder(); |
158 | builder.append("pred ").append(name()).append("("); | 156 | builder.append("pred ").append(name()).append("("); |
159 | var parameterIterator = parameters.iterator(); | 157 | var parameterIterator = symbolicParameters.iterator(); |
160 | if (parameterIterator.hasNext()) { | 158 | if (parameterIterator.hasNext()) { |
161 | builder.append(parameterIterator.next()); | 159 | builder.append(parameterIterator.next()); |
162 | while (parameterIterator.hasNext()) { | 160 | while (parameterIterator.hasNext()) { |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java index a42ae558..3fac4627 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java | |||
@@ -7,20 +7,16 @@ package tools.refinery.store.query.dnf; | |||
7 | 7 | ||
8 | import tools.refinery.store.query.dnf.callback.*; | 8 | import tools.refinery.store.query.dnf.callback.*; |
9 | import tools.refinery.store.query.literal.Literal; | 9 | import tools.refinery.store.query.literal.Literal; |
10 | import tools.refinery.store.query.term.DataVariable; | 10 | import tools.refinery.store.query.term.*; |
11 | import tools.refinery.store.query.term.NodeVariable; | ||
12 | import tools.refinery.store.query.term.Variable; | ||
13 | 11 | ||
14 | import java.util.*; | 12 | import java.util.*; |
15 | 13 | ||
16 | @SuppressWarnings("UnusedReturnValue") | 14 | @SuppressWarnings("UnusedReturnValue") |
17 | public final class DnfBuilder { | 15 | public final class DnfBuilder { |
18 | private final String name; | 16 | private final String name; |
19 | |||
20 | private final List<Variable> parameters = new ArrayList<>(); | 17 | private final List<Variable> parameters = new ArrayList<>(); |
21 | 18 | private final Map<Variable, ParameterDirection> directions = new HashMap<>(); | |
22 | private final List<FunctionalDependency<Variable>> functionalDependencies = new ArrayList<>(); | 19 | private final List<FunctionalDependency<Variable>> functionalDependencies = new ArrayList<>(); |
23 | |||
24 | private final List<List<Literal>> clauses = new ArrayList<>(); | 20 | private final List<List<Literal>> clauses = new ArrayList<>(); |
25 | 21 | ||
26 | DnfBuilder(String name) { | 22 | DnfBuilder(String name) { |
@@ -37,6 +33,18 @@ public final class DnfBuilder { | |||
37 | return variable; | 33 | return variable; |
38 | } | 34 | } |
39 | 35 | ||
36 | public NodeVariable parameter(ParameterDirection direction) { | ||
37 | var variable = parameter(); | ||
38 | putDirection(variable, direction); | ||
39 | return variable; | ||
40 | } | ||
41 | |||
42 | public NodeVariable parameter(String name, ParameterDirection direction) { | ||
43 | var variable = parameter(name); | ||
44 | putDirection(variable, direction); | ||
45 | return variable; | ||
46 | } | ||
47 | |||
40 | public <T> DataVariable<T> parameter(Class<T> type) { | 48 | public <T> DataVariable<T> parameter(Class<T> type) { |
41 | return parameter(null, type); | 49 | return parameter(null, type); |
42 | } | 50 | } |
@@ -47,6 +55,18 @@ public final class DnfBuilder { | |||
47 | return variable; | 55 | return variable; |
48 | } | 56 | } |
49 | 57 | ||
58 | public <T> DataVariable<T> parameter(Class<T> type, ParameterDirection direction) { | ||
59 | var variable = parameter(type); | ||
60 | putDirection(variable, direction); | ||
61 | return variable; | ||
62 | } | ||
63 | |||
64 | public <T> DataVariable<T> parameter(String name, Class<T> type, ParameterDirection direction) { | ||
65 | var variable = parameter(name, type); | ||
66 | putDirection(variable, direction); | ||
67 | return variable; | ||
68 | } | ||
69 | |||
50 | public DnfBuilder parameter(Variable variable) { | 70 | public DnfBuilder parameter(Variable variable) { |
51 | if (parameters.contains(variable)) { | 71 | if (parameters.contains(variable)) { |
52 | throw new IllegalArgumentException("Duplicate parameter: " + variable); | 72 | throw new IllegalArgumentException("Duplicate parameter: " + variable); |
@@ -55,12 +75,49 @@ public final class DnfBuilder { | |||
55 | return this; | 75 | return this; |
56 | } | 76 | } |
57 | 77 | ||
78 | public DnfBuilder parameter(Variable variable, ParameterDirection direction) { | ||
79 | parameter(variable); | ||
80 | putDirection(variable, direction); | ||
81 | return this; | ||
82 | } | ||
83 | |||
84 | private void putDirection(Variable variable, ParameterDirection direction) { | ||
85 | if (variable.tryGetType().isPresent()) { | ||
86 | if (direction == ParameterDirection.IN_OUT) { | ||
87 | throw new IllegalArgumentException("%s direction is forbidden for data variable %s" | ||
88 | .formatted(direction, variable)); | ||
89 | } | ||
90 | } else { | ||
91 | if (direction == ParameterDirection.OUT) { | ||
92 | throw new IllegalArgumentException("%s direction is forbidden for node variable %s" | ||
93 | .formatted(direction, variable)); | ||
94 | } | ||
95 | } | ||
96 | directions.put(variable, direction); | ||
97 | } | ||
98 | |||
58 | public DnfBuilder parameters(Variable... variables) { | 99 | public DnfBuilder parameters(Variable... variables) { |
59 | return parameters(List.of(variables)); | 100 | return parameters(List.of(variables)); |
60 | } | 101 | } |
61 | 102 | ||
62 | public DnfBuilder parameters(Collection<? extends Variable> variables) { | 103 | public DnfBuilder parameters(Collection<? extends Variable> variables) { |
63 | parameters.addAll(variables); | 104 | for (var variable : variables) { |
105 | parameter(variable); | ||
106 | } | ||
107 | return this; | ||
108 | } | ||
109 | |||
110 | public DnfBuilder parameters(Collection<? extends Variable> variables, ParameterDirection direction) { | ||
111 | for (var variable : variables) { | ||
112 | parameter(variable, direction); | ||
113 | } | ||
114 | return this; | ||
115 | } | ||
116 | |||
117 | public DnfBuilder symbolicParameters(Collection<SymbolicParameter> parameters) { | ||
118 | for (var parameter : parameters) { | ||
119 | parameter(parameter.getVariable(), parameter.getDirection()); | ||
120 | } | ||
64 | return this; | 121 | return this; |
65 | } | 122 | } |
66 | 123 | ||
@@ -152,54 +209,98 @@ public final class DnfBuilder { | |||
152 | } | 209 | } |
153 | 210 | ||
154 | public DnfBuilder clause(Collection<? extends Literal> literals) { | 211 | public DnfBuilder clause(Collection<? extends Literal> literals) { |
155 | // Remove duplicates by using a hashed data structure. | 212 | clauses.add(List.copyOf(literals)); |
156 | var filteredLiterals = new LinkedHashSet<Literal>(literals.size()); | ||
157 | for (var literal : literals) { | ||
158 | var reduction = literal.getReduction(); | ||
159 | switch (reduction) { | ||
160 | case NOT_REDUCIBLE -> filteredLiterals.add(literal); | ||
161 | case ALWAYS_TRUE -> { | ||
162 | // Literals reducible to {@code true} can be omitted, because the model is always assumed to have at | ||
163 | // least on object. | ||
164 | } | ||
165 | case ALWAYS_FALSE -> { | ||
166 | // Clauses with {@code false} literals can be omitted entirely. | ||
167 | return this; | ||
168 | } | ||
169 | default -> throw new IllegalArgumentException("Invalid reduction: " + reduction); | ||
170 | } | ||
171 | } | ||
172 | clauses.add(List.copyOf(filteredLiterals)); | ||
173 | return this; | 213 | return this; |
174 | } | 214 | } |
175 | 215 | ||
216 | <T> void output(DataVariable<T> outputVariable) { | ||
217 | var fromParameters = Set.copyOf(parameters); | ||
218 | parameter(outputVariable, ParameterDirection.OUT); | ||
219 | functionalDependency(fromParameters, Set.of(outputVariable)); | ||
220 | } | ||
221 | |||
176 | public Dnf build() { | 222 | public Dnf build() { |
177 | var postProcessedClauses = postProcessClauses(); | 223 | var postProcessedClauses = postProcessClauses(); |
178 | return new Dnf(name, Collections.unmodifiableList(parameters), | 224 | return new Dnf(name, createParameterList(postProcessedClauses), |
179 | Collections.unmodifiableList(functionalDependencies), | 225 | Collections.unmodifiableList(functionalDependencies), |
180 | Collections.unmodifiableList(postProcessedClauses)); | 226 | Collections.unmodifiableList(postProcessedClauses)); |
181 | } | 227 | } |
182 | 228 | ||
183 | <T> void output(DataVariable<T> outputVariable) { | ||
184 | functionalDependency(Set.copyOf(parameters), Set.of(outputVariable)); | ||
185 | parameter(outputVariable); | ||
186 | } | ||
187 | |||
188 | private List<DnfClause> postProcessClauses() { | 229 | private List<DnfClause> postProcessClauses() { |
230 | var parameterSet = Collections.unmodifiableSet(new LinkedHashSet<>(parameters)); | ||
231 | var parameterWeights = getParameterWeights(); | ||
189 | var postProcessedClauses = new ArrayList<DnfClause>(clauses.size()); | 232 | var postProcessedClauses = new ArrayList<DnfClause>(clauses.size()); |
190 | for (var literals : clauses) { | 233 | for (var literals : clauses) { |
191 | if (literals.isEmpty()) { | 234 | var postProcessor = new ClausePostProcessor(parameterSet, parameterWeights, literals); |
192 | // Predicate will always match, the other clauses are irrelevant. | 235 | var result = postProcessor.postProcessClause(); |
193 | return List.of(new DnfClause(Set.of(), List.of())); | 236 | if (result instanceof ClausePostProcessor.ClauseResult clauseResult) { |
194 | } | 237 | postProcessedClauses.add(clauseResult.clause()); |
195 | var variables = new HashSet<Variable>(); | 238 | } else if (result instanceof ClausePostProcessor.ConstantResult constantResult) { |
196 | for (var literal : literals) { | 239 | switch (constantResult) { |
197 | variables.addAll(literal.getBoundVariables()); | 240 | case ALWAYS_TRUE -> { |
241 | return List.of(new DnfClause(Set.of(), List.of())); | ||
242 | } | ||
243 | case ALWAYS_FALSE -> { | ||
244 | // Skip this clause because it can never match. | ||
245 | } | ||
246 | default -> throw new IllegalStateException("Unexpected ClausePostProcessor.ConstantResult: " + | ||
247 | constantResult); | ||
248 | } | ||
249 | } else { | ||
250 | throw new IllegalStateException("Unexpected ClausePostProcessor.Result: " + result); | ||
198 | } | 251 | } |
199 | parameters.forEach(variables::remove); | ||
200 | postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables), | ||
201 | Collections.unmodifiableList(literals))); | ||
202 | } | 252 | } |
203 | return postProcessedClauses; | 253 | return postProcessedClauses; |
204 | } | 254 | } |
255 | |||
256 | private Map<Variable, Integer> getParameterWeights() { | ||
257 | var mutableParameterWeights = new HashMap<Variable, Integer>(); | ||
258 | int arity = parameters.size(); | ||
259 | for (int i = 0; i < arity; i++) { | ||
260 | mutableParameterWeights.put(parameters.get(i), i); | ||
261 | } | ||
262 | return Collections.unmodifiableMap(mutableParameterWeights); | ||
263 | } | ||
264 | |||
265 | private List<SymbolicParameter> createParameterList(List<DnfClause> postProcessedClauses) { | ||
266 | var outputParameterVariables = new HashSet<>(parameters); | ||
267 | for (var clause : postProcessedClauses) { | ||
268 | outputParameterVariables.retainAll(clause.positiveVariables()); | ||
269 | } | ||
270 | var parameterList = new ArrayList<SymbolicParameter>(parameters.size()); | ||
271 | for (var parameter : parameters) { | ||
272 | ParameterDirection direction = getDirection(outputParameterVariables, parameter); | ||
273 | parameterList.add(new SymbolicParameter(parameter, direction)); | ||
274 | } | ||
275 | return Collections.unmodifiableList(parameterList); | ||
276 | } | ||
277 | |||
278 | private ParameterDirection getDirection(HashSet<Variable> outputParameterVariables, Variable parameter) { | ||
279 | var direction = getInferredDirection(outputParameterVariables, parameter); | ||
280 | var expectedDirection = directions.get(parameter); | ||
281 | if (expectedDirection == ParameterDirection.IN && direction == ParameterDirection.IN_OUT) { | ||
282 | // Parameters may be explicitly marked as {@code @In} even if they are bound in all clauses. | ||
283 | return expectedDirection; | ||
284 | } | ||
285 | if (expectedDirection != null && expectedDirection != direction) { | ||
286 | throw new IllegalArgumentException("Expected parameter %s to have direction %s, but got %s instead" | ||
287 | .formatted(parameter, expectedDirection, direction)); | ||
288 | } | ||
289 | return direction; | ||
290 | } | ||
291 | |||
292 | private static ParameterDirection getInferredDirection(HashSet<Variable> outputParameterVariables, | ||
293 | Variable parameter) { | ||
294 | if (outputParameterVariables.contains(parameter)) { | ||
295 | if (parameter instanceof NodeVariable) { | ||
296 | return ParameterDirection.IN_OUT; | ||
297 | } else if (parameter instanceof AnyDataVariable) { | ||
298 | return ParameterDirection.OUT; | ||
299 | } else { | ||
300 | throw new IllegalArgumentException("Unknown parameter: " + parameter); | ||
301 | } | ||
302 | } else { | ||
303 | return ParameterDirection.IN; | ||
304 | } | ||
305 | } | ||
205 | } | 306 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java index a01d7d55..fdd0d47c 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java | |||
@@ -12,7 +12,7 @@ import tools.refinery.store.query.term.Variable; | |||
12 | import java.util.List; | 12 | import java.util.List; |
13 | import java.util.Set; | 13 | import java.util.Set; |
14 | 14 | ||
15 | public record DnfClause(Set<Variable> boundVariables, List<Literal> literals) { | 15 | public record DnfClause(Set<Variable> positiveVariables, List<Literal> literals) { |
16 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, DnfClause other) { | 16 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, DnfClause other) { |
17 | int size = literals.size(); | 17 | int size = literals.size(); |
18 | if (size != other.literals.size()) { | 18 | if (size != other.literals.size()) { |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQuery.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQuery.java index 680fa631..57cb8baf 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQuery.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQuery.java | |||
@@ -17,20 +17,21 @@ public final class FunctionalQuery<T> implements Query<T> { | |||
17 | private final Class<T> type; | 17 | private final Class<T> type; |
18 | 18 | ||
19 | FunctionalQuery(Dnf dnf, Class<T> type) { | 19 | FunctionalQuery(Dnf dnf, Class<T> type) { |
20 | var parameters = dnf.getParameters(); | 20 | var parameters = dnf.getSymbolicParameters(); |
21 | int outputIndex = dnf.arity() - 1; | 21 | int outputIndex = dnf.arity() - 1; |
22 | for (int i = 0; i < outputIndex; i++) { | 22 | for (int i = 0; i < outputIndex; i++) { |
23 | var parameter = parameters.get(i); | 23 | var parameter = parameters.get(i); |
24 | if (!(parameter instanceof NodeVariable)) { | 24 | var parameterType = parameter.tryGetType(); |
25 | throw new IllegalArgumentException("Expected parameter %s of %s to be of sort %s, but got %s instead" | 25 | if (parameterType.isPresent()) { |
26 | .formatted(parameter, dnf, NodeSort.INSTANCE, parameter.getSort())); | 26 | throw new IllegalArgumentException("Expected parameter %s of %s to be a node variable, got %s instead" |
27 | .formatted(parameter, dnf, parameterType.get().getName())); | ||
27 | } | 28 | } |
28 | } | 29 | } |
29 | var outputParameter = parameters.get(outputIndex); | 30 | var outputParameter = parameters.get(outputIndex); |
30 | if (!(outputParameter instanceof DataVariable<?> dataOutputParameter) || | 31 | var outputParameterType = outputParameter.tryGetType(); |
31 | !dataOutputParameter.getType().equals(type)) { | 32 | if (outputParameterType.isEmpty() || !outputParameterType.get().equals(type)) { |
32 | throw new IllegalArgumentException("Expected parameter %s of %s to be of sort %s, but got %s instead" | 33 | throw new IllegalArgumentException("Expected parameter %s of %s to be %s, but got %s instead".formatted( |
33 | .formatted(outputParameter, dnf, type, outputParameter.getSort())); | 34 | outputParameter, dnf, type, outputParameterType.map(Class::getName).orElse("node"))); |
34 | } | 35 | } |
35 | this.dnf = dnf; | 36 | this.dnf = dnf; |
36 | this.type = type; | 37 | this.type = type; |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/RelationalQuery.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/RelationalQuery.java index 0741d8d9..c043a285 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/RelationalQuery.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/RelationalQuery.java | |||
@@ -8,7 +8,6 @@ package tools.refinery.store.query.dnf; | |||
8 | import tools.refinery.store.query.literal.CallLiteral; | 8 | import tools.refinery.store.query.literal.CallLiteral; |
9 | import tools.refinery.store.query.literal.CallPolarity; | 9 | import tools.refinery.store.query.literal.CallPolarity; |
10 | import tools.refinery.store.query.term.AssignedValue; | 10 | import tools.refinery.store.query.term.AssignedValue; |
11 | import tools.refinery.store.query.term.NodeSort; | ||
12 | import tools.refinery.store.query.term.NodeVariable; | 11 | import tools.refinery.store.query.term.NodeVariable; |
13 | 12 | ||
14 | import java.util.Collections; | 13 | import java.util.Collections; |
@@ -19,10 +18,11 @@ public final class RelationalQuery implements Query<Boolean> { | |||
19 | private final Dnf dnf; | 18 | private final Dnf dnf; |
20 | 19 | ||
21 | RelationalQuery(Dnf dnf) { | 20 | RelationalQuery(Dnf dnf) { |
22 | for (var parameter : dnf.getParameters()) { | 21 | for (var parameter : dnf.getSymbolicParameters()) { |
23 | if (!(parameter instanceof NodeVariable)) { | 22 | var parameterType = parameter.tryGetType(); |
24 | throw new IllegalArgumentException("Expected parameter %s of %s to be of sort %s, but got %s instead" | 23 | if (parameterType.isPresent()) { |
25 | .formatted(parameter, dnf, NodeSort.INSTANCE, parameter.getSort())); | 24 | throw new IllegalArgumentException("Expected parameter %s of %s to be a node variable, got %s instead" |
25 | .formatted(parameter, dnf, parameterType.get().getName())); | ||
26 | } | 26 | } |
27 | } | 27 | } |
28 | this.dnf = dnf; | 28 | this.dnf = dnf; |
@@ -77,7 +77,6 @@ public final class RelationalQuery implements Query<Boolean> { | |||
77 | return dnf.count(arguments); | 77 | return dnf.count(arguments); |
78 | } | 78 | } |
79 | 79 | ||
80 | |||
81 | @Override | 80 | @Override |
82 | public boolean equals(Object o) { | 81 | public boolean equals(Object o) { |
83 | if (this == o) return true; | 82 | if (this == o) return true; |
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 new file mode 100644 index 00000000..e2f05bde --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/SymbolicParameter.java | |||
@@ -0,0 +1,48 @@ | |||
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.dnf; | ||
7 | |||
8 | import tools.refinery.store.query.term.Parameter; | ||
9 | import tools.refinery.store.query.term.ParameterDirection; | ||
10 | import tools.refinery.store.query.term.Variable; | ||
11 | |||
12 | import java.util.Objects; | ||
13 | |||
14 | public final class SymbolicParameter extends Parameter { | ||
15 | private final Variable variable; | ||
16 | |||
17 | public SymbolicParameter(Variable variable, ParameterDirection direction) { | ||
18 | super(variable.tryGetType().orElse(null), direction); | ||
19 | this.variable = variable; | ||
20 | } | ||
21 | |||
22 | public Variable getVariable() { | ||
23 | return variable; | ||
24 | } | ||
25 | |||
26 | @Override | ||
27 | public String toString() { | ||
28 | var direction = getDirection(); | ||
29 | if (direction == ParameterDirection.IN_OUT) { | ||
30 | return variable.toString(); | ||
31 | } | ||
32 | return "%s %s".formatted(getDirection(), variable); | ||
33 | } | ||
34 | |||
35 | @Override | ||
36 | public boolean equals(Object o) { | ||
37 | if (this == o) return true; | ||
38 | if (o == null || getClass() != o.getClass()) return false; | ||
39 | if (!super.equals(o)) return false; | ||
40 | SymbolicParameter that = (SymbolicParameter) o; | ||
41 | return Objects.equals(variable, that.variable); | ||
42 | } | ||
43 | |||
44 | @Override | ||
45 | public int hashCode() { | ||
46 | return Objects.hash(super.hashCode(), variable); | ||
47 | } | ||
48 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java index 0f6ee6c2..9315fb30 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java | |||
@@ -6,6 +6,7 @@ | |||
6 | package tools.refinery.store.query.equality; | 6 | package tools.refinery.store.query.equality; |
7 | 7 | ||
8 | import tools.refinery.store.query.dnf.Dnf; | 8 | import tools.refinery.store.query.dnf.Dnf; |
9 | import tools.refinery.store.query.dnf.SymbolicParameter; | ||
9 | import tools.refinery.store.query.term.Variable; | 10 | import tools.refinery.store.query.term.Variable; |
10 | 11 | ||
11 | import java.util.HashMap; | 12 | import java.util.HashMap; |
@@ -17,8 +18,8 @@ public class LiteralEqualityHelper { | |||
17 | private final Map<Variable, Variable> leftToRight; | 18 | private final Map<Variable, Variable> leftToRight; |
18 | private final Map<Variable, Variable> rightToLeft; | 19 | private final Map<Variable, Variable> rightToLeft; |
19 | 20 | ||
20 | public LiteralEqualityHelper(DnfEqualityChecker dnfEqualityChecker, List<Variable> leftParameters, | 21 | public LiteralEqualityHelper(DnfEqualityChecker dnfEqualityChecker, List<SymbolicParameter> leftParameters, |
21 | List<Variable> rightParameters) { | 22 | List<SymbolicParameter> rightParameters) { |
22 | this.dnfEqualityChecker = dnfEqualityChecker; | 23 | this.dnfEqualityChecker = dnfEqualityChecker; |
23 | var arity = leftParameters.size(); | 24 | var arity = leftParameters.size(); |
24 | if (arity != rightParameters.size()) { | 25 | if (arity != rightParameters.size()) { |
@@ -27,7 +28,7 @@ public class LiteralEqualityHelper { | |||
27 | leftToRight = new HashMap<>(arity); | 28 | leftToRight = new HashMap<>(arity); |
28 | rightToLeft = new HashMap<>(arity); | 29 | rightToLeft = new HashMap<>(arity); |
29 | for (int i = 0; i < arity; i++) { | 30 | for (int i = 0; i < arity; i++) { |
30 | if (!variableEqual(leftParameters.get(i), rightParameters.get(i))) { | 31 | if (!variableEqual(leftParameters.get(i).getVariable(), rightParameters.get(i).getVariable())) { |
31 | throw new IllegalArgumentException("Parameter lists cannot be unified: duplicate parameter " + i); | 32 | throw new IllegalArgumentException("Parameter lists cannot be unified: duplicate parameter " + i); |
32 | } | 33 | } |
33 | } | 34 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/exceptions/IncompatibleParameterDirectionException.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/exceptions/IncompatibleParameterDirectionException.java new file mode 100644 index 00000000..52da20ae --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/exceptions/IncompatibleParameterDirectionException.java | |||
@@ -0,0 +1,16 @@ | |||
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.exceptions; | ||
7 | |||
8 | public class IncompatibleParameterDirectionException extends RuntimeException { | ||
9 | public IncompatibleParameterDirectionException(String message) { | ||
10 | super(message); | ||
11 | } | ||
12 | |||
13 | public IncompatibleParameterDirectionException(String message, Throwable cause) { | ||
14 | super(message, cause); | ||
15 | } | ||
16 | } | ||
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 b08c1037..55db04e0 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 | |||
@@ -25,13 +25,13 @@ public abstract class AbstractCallLiteral implements Literal { | |||
25 | } | 25 | } |
26 | this.target = target; | 26 | this.target = target; |
27 | this.arguments = arguments; | 27 | this.arguments = arguments; |
28 | var sorts = target.getSorts(); | 28 | var parameters = target.getParameters(); |
29 | for (int i = 0; i < arity; i++) { | 29 | for (int i = 0; i < arity; i++) { |
30 | var argument = arguments.get(i); | 30 | var argument = arguments.get(i); |
31 | var sort = sorts.get(i); | 31 | var parameter = parameters.get(i); |
32 | if (!sort.isInstance(argument)) { | 32 | if (!parameter.isAssignable(argument)) { |
33 | throw new IllegalArgumentException("Required argument %d of %s to be of sort %s, but got %s instead" | 33 | throw new IllegalArgumentException("Argument %d of %s is not assignable to parameter %s" |
34 | .formatted(i, target, sort, argument.getSort())); | 34 | .formatted(i, target, parameter)); |
35 | } | 35 | } |
36 | } | 36 | } |
37 | } | 37 | } |
@@ -80,6 +80,6 @@ public abstract class AbstractCallLiteral implements Literal { | |||
80 | 80 | ||
81 | @Override | 81 | @Override |
82 | public int hashCode() { | 82 | public int hashCode() { |
83 | return Objects.hash(target, arguments); | 83 | return Objects.hash(getClass(), target, arguments); |
84 | } | 84 | } |
85 | } | 85 | } |
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 93e59291..2aa0a0d5 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 | |||
@@ -14,12 +14,12 @@ import tools.refinery.store.query.term.Variable; | |||
14 | 14 | ||
15 | import java.util.List; | 15 | import java.util.List; |
16 | import java.util.Objects; | 16 | import java.util.Objects; |
17 | import java.util.Set; | ||
18 | 17 | ||
19 | public class AggregationLiteral<R, T> extends AbstractCallLiteral { | 18 | public class AggregationLiteral<R, T> extends AbstractCallLiteral { |
20 | private final DataVariable<R> resultVariable; | 19 | private final DataVariable<R> resultVariable; |
21 | private final DataVariable<T> inputVariable; | 20 | private final DataVariable<T> inputVariable; |
22 | private final Aggregator<R, T> aggregator; | 21 | private final Aggregator<R, T> aggregator; |
22 | private final VariableBinder variableBinder; | ||
23 | 23 | ||
24 | public AggregationLiteral(DataVariable<R> resultVariable, Aggregator<R, T> aggregator, | 24 | public AggregationLiteral(DataVariable<R> resultVariable, Aggregator<R, T> aggregator, |
25 | DataVariable<T> inputVariable, Constraint target, List<Variable> arguments) { | 25 | DataVariable<T> inputVariable, Constraint target, List<Variable> arguments) { |
@@ -32,10 +32,6 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral { | |||
32 | throw new IllegalArgumentException("Result variable %s must of type %s, got %s instead".formatted( | 32 | throw new IllegalArgumentException("Result variable %s must of type %s, got %s instead".formatted( |
33 | resultVariable, aggregator.getResultType().getName(), resultVariable.getType().getName())); | 33 | resultVariable, aggregator.getResultType().getName(), resultVariable.getType().getName())); |
34 | } | 34 | } |
35 | if (!arguments.contains(inputVariable)) { | ||
36 | throw new IllegalArgumentException("Input variable %s must appear in the argument list".formatted( | ||
37 | inputVariable)); | ||
38 | } | ||
39 | if (arguments.contains(resultVariable)) { | 35 | if (arguments.contains(resultVariable)) { |
40 | throw new IllegalArgumentException("Result variable %s must not appear in the argument list".formatted( | 36 | throw new IllegalArgumentException("Result variable %s must not appear in the argument list".formatted( |
41 | resultVariable)); | 37 | resultVariable)); |
@@ -43,6 +39,14 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral { | |||
43 | this.resultVariable = resultVariable; | 39 | this.resultVariable = resultVariable; |
44 | this.inputVariable = inputVariable; | 40 | this.inputVariable = inputVariable; |
45 | this.aggregator = aggregator; | 41 | this.aggregator = aggregator; |
42 | variableBinder = VariableBinder.builder() | ||
43 | .variable(resultVariable, VariableDirection.OUT) | ||
44 | .parameterList(false, target.getParameters(), arguments) | ||
45 | .build(); | ||
46 | if (variableBinder.getDirection(inputVariable) != VariableDirection.CLOSURE) { | ||
47 | throw new IllegalArgumentException("Input variable %s must appear in the argument list".formatted( | ||
48 | inputVariable)); | ||
49 | } | ||
46 | } | 50 | } |
47 | 51 | ||
48 | public DataVariable<R> getResultVariable() { | 52 | public DataVariable<R> getResultVariable() { |
@@ -58,8 +62,8 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral { | |||
58 | } | 62 | } |
59 | 63 | ||
60 | @Override | 64 | @Override |
61 | public Set<Variable> getBoundVariables() { | 65 | public VariableBinder getVariableBinder() { |
62 | return Set.of(resultVariable); | 66 | return variableBinder; |
63 | } | 67 | } |
64 | 68 | ||
65 | @Override | 69 | @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 8cc3fae6..4da92b90 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 | |||
@@ -9,21 +9,43 @@ import tools.refinery.store.query.equality.LiteralEqualityHelper; | |||
9 | import tools.refinery.store.query.substitution.Substitution; | 9 | import tools.refinery.store.query.substitution.Substitution; |
10 | import tools.refinery.store.query.term.DataVariable; | 10 | import tools.refinery.store.query.term.DataVariable; |
11 | import tools.refinery.store.query.term.Term; | 11 | import tools.refinery.store.query.term.Term; |
12 | import tools.refinery.store.query.term.Variable; | ||
13 | 12 | ||
14 | import java.util.Set; | 13 | import java.util.Objects; |
15 | 14 | ||
16 | public record AssignLiteral<T>(DataVariable<T> variable, Term<T> term) implements Literal { | 15 | public final class AssignLiteral<T> implements Literal { |
17 | public AssignLiteral { | 16 | private final DataVariable<T> variable; |
17 | private final Term<T> term; | ||
18 | private final VariableBinder variableBinder; | ||
19 | |||
20 | public AssignLiteral(DataVariable<T> variable, Term<T> term) { | ||
18 | if (!term.getType().equals(variable.getType())) { | 21 | if (!term.getType().equals(variable.getType())) { |
19 | throw new IllegalArgumentException("Term %s must be of type %s, got %s instead".formatted( | 22 | throw new IllegalArgumentException("Term %s must be of type %s, got %s instead".formatted( |
20 | term, variable.getType().getName(), term.getType().getName())); | 23 | term, variable.getType().getName(), term.getType().getName())); |
21 | } | 24 | } |
25 | this.variable = variable; | ||
26 | this.term = term; | ||
27 | var inputVariables = term.getInputVariables(); | ||
28 | if (inputVariables.contains(variable)) { | ||
29 | throw new IllegalArgumentException("Result variable %s must not appear in the term %s".formatted( | ||
30 | variable, term)); | ||
31 | } | ||
32 | variableBinder = VariableBinder.builder() | ||
33 | .variable(variable, VariableDirection.OUT) | ||
34 | .variables(inputVariables, VariableDirection.IN) | ||
35 | .build(); | ||
36 | } | ||
37 | |||
38 | public DataVariable<T> getTargetVariable() { | ||
39 | return variable; | ||
40 | } | ||
41 | |||
42 | public Term<T> getTerm() { | ||
43 | return term; | ||
22 | } | 44 | } |
23 | 45 | ||
24 | @Override | 46 | @Override |
25 | public Set<Variable> getBoundVariables() { | 47 | public VariableBinder getVariableBinder() { |
26 | return Set.of(variable); | 48 | return variableBinder; |
27 | } | 49 | } |
28 | 50 | ||
29 | @Override | 51 | @Override |
@@ -41,9 +63,22 @@ public record AssignLiteral<T>(DataVariable<T> variable, Term<T> term) implement | |||
41 | otherLetLiteral.term); | 63 | otherLetLiteral.term); |
42 | } | 64 | } |
43 | 65 | ||
44 | |||
45 | @Override | 66 | @Override |
46 | public String toString() { | 67 | public String toString() { |
47 | return "%s is (%s)".formatted(variable, term); | 68 | return "%s is (%s)".formatted(variable, term); |
48 | } | 69 | } |
70 | |||
71 | @Override | ||
72 | public boolean equals(Object obj) { | ||
73 | if (obj == this) return true; | ||
74 | if (obj == null || obj.getClass() != this.getClass()) return false; | ||
75 | var that = (AssignLiteral<?>) obj; | ||
76 | return Objects.equals(this.variable, that.variable) && | ||
77 | Objects.equals(this.term, that.term); | ||
78 | } | ||
79 | |||
80 | @Override | ||
81 | public int hashCode() { | ||
82 | return Objects.hash(getClass(), variable, term); | ||
83 | } | ||
49 | } | 84 | } |
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 59538831..61486e4c 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 | |||
@@ -9,21 +9,31 @@ import tools.refinery.store.query.equality.LiteralEqualityHelper; | |||
9 | import tools.refinery.store.query.substitution.Substitution; | 9 | import tools.refinery.store.query.substitution.Substitution; |
10 | import tools.refinery.store.query.term.ConstantTerm; | 10 | import tools.refinery.store.query.term.ConstantTerm; |
11 | import tools.refinery.store.query.term.Term; | 11 | import tools.refinery.store.query.term.Term; |
12 | import tools.refinery.store.query.term.Variable; | ||
13 | 12 | ||
14 | import java.util.Set; | 13 | import java.util.Objects; |
15 | 14 | ||
16 | public record AssumeLiteral(Term<Boolean> term) implements Literal { | 15 | public final class AssumeLiteral implements Literal { |
17 | public AssumeLiteral { | 16 | private final Term<Boolean> term; |
17 | private final VariableBinder variableBinder; | ||
18 | |||
19 | public AssumeLiteral(Term<Boolean> term) { | ||
18 | if (!term.getType().equals(Boolean.class)) { | 20 | if (!term.getType().equals(Boolean.class)) { |
19 | throw new IllegalArgumentException("Term %s must be of type %s, got %s instead".formatted( | 21 | throw new IllegalArgumentException("Term %s must be of type %s, got %s instead".formatted( |
20 | term, Boolean.class.getName(), term.getType().getName())); | 22 | term, Boolean.class.getName(), term.getType().getName())); |
21 | } | 23 | } |
24 | this.term = term; | ||
25 | variableBinder = VariableBinder.builder() | ||
26 | .variables(term.getInputVariables(), VariableDirection.IN) | ||
27 | .build(); | ||
28 | } | ||
29 | |||
30 | public Term<Boolean> getTerm() { | ||
31 | return term; | ||
22 | } | 32 | } |
23 | 33 | ||
24 | @Override | 34 | @Override |
25 | public Set<Variable> getBoundVariables() { | 35 | public VariableBinder getVariableBinder() { |
26 | return Set.of(); | 36 | return variableBinder; |
27 | } | 37 | } |
28 | 38 | ||
29 | @Override | 39 | @Override |
@@ -54,4 +64,17 @@ public record AssumeLiteral(Term<Boolean> term) implements Literal { | |||
54 | public String toString() { | 64 | public String toString() { |
55 | return "(%s)".formatted(term); | 65 | return "(%s)".formatted(term); |
56 | } | 66 | } |
67 | |||
68 | @Override | ||
69 | public boolean equals(Object obj) { | ||
70 | if (obj == this) return true; | ||
71 | if (obj == null || obj.getClass() != this.getClass()) return false; | ||
72 | var that = (AssumeLiteral) obj; | ||
73 | return Objects.equals(this.term, that.term); | ||
74 | } | ||
75 | |||
76 | @Override | ||
77 | public int hashCode() { | ||
78 | return Objects.hash(getClass(), term); | ||
79 | } | ||
57 | } | 80 | } |
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 a32cfd80..e61f0535 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 | |||
@@ -5,12 +5,9 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.query.literal; | 6 | package tools.refinery.store.query.literal; |
7 | 7 | ||
8 | import tools.refinery.store.query.term.Variable; | ||
9 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | 8 | import tools.refinery.store.query.equality.LiteralEqualityHelper; |
10 | import tools.refinery.store.query.substitution.Substitution; | 9 | import tools.refinery.store.query.substitution.Substitution; |
11 | 10 | ||
12 | import java.util.Set; | ||
13 | |||
14 | public enum BooleanLiteral implements CanNegate<BooleanLiteral> { | 11 | public enum BooleanLiteral implements CanNegate<BooleanLiteral> { |
15 | TRUE(true), | 12 | TRUE(true), |
16 | FALSE(false); | 13 | FALSE(false); |
@@ -22,8 +19,8 @@ public enum BooleanLiteral implements CanNegate<BooleanLiteral> { | |||
22 | } | 19 | } |
23 | 20 | ||
24 | @Override | 21 | @Override |
25 | public Set<Variable> getBoundVariables() { | 22 | public VariableBinder getVariableBinder() { |
26 | return Set.of(); | 23 | return VariableBinder.EMPTY; |
27 | } | 24 | } |
28 | 25 | ||
29 | @Override | 26 | @Override |
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 82088c8b..dc6098a8 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 | |||
@@ -8,28 +8,31 @@ package tools.refinery.store.query.literal; | |||
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.substitution.Substitution; | 10 | import tools.refinery.store.query.substitution.Substitution; |
11 | import tools.refinery.store.query.term.NodeSort; | ||
12 | import tools.refinery.store.query.term.Variable; | 11 | import tools.refinery.store.query.term.Variable; |
13 | 12 | ||
14 | import java.util.List; | 13 | import java.util.List; |
15 | import java.util.Objects; | 14 | import java.util.Objects; |
16 | import java.util.Set; | ||
17 | 15 | ||
18 | public final class CallLiteral extends AbstractCallLiteral implements CanNegate<CallLiteral> { | 16 | public final class CallLiteral extends AbstractCallLiteral implements CanNegate<CallLiteral> { |
19 | private final CallPolarity polarity; | 17 | private final CallPolarity polarity; |
18 | private final VariableBinder variableBinder; | ||
20 | 19 | ||
21 | public CallLiteral(CallPolarity polarity, Constraint target, List<Variable> arguments) { | 20 | public CallLiteral(CallPolarity polarity, Constraint target, List<Variable> arguments) { |
22 | super(target, arguments); | 21 | super(target, arguments); |
22 | var parameters = target.getParameters(); | ||
23 | int arity = target.arity(); | ||
23 | if (polarity.isTransitive()) { | 24 | if (polarity.isTransitive()) { |
24 | if (target.arity() != 2) { | 25 | if (arity != 2) { |
25 | throw new IllegalArgumentException("Transitive closures can only take binary relations"); | 26 | throw new IllegalArgumentException("Transitive closures can only take binary relations"); |
26 | } | 27 | } |
27 | var sorts = target.getSorts(); | 28 | if (parameters.get(0).isDataVariable() || parameters.get(1).isDataVariable()) { |
28 | if (!sorts.get(0).equals(NodeSort.INSTANCE) || !sorts.get(1).equals(NodeSort.INSTANCE)) { | ||
29 | throw new IllegalArgumentException("Transitive closures can only be computed over nodes"); | 29 | throw new IllegalArgumentException("Transitive closures can only be computed over nodes"); |
30 | } | 30 | } |
31 | } | 31 | } |
32 | this.polarity = polarity; | 32 | this.polarity = polarity; |
33 | variableBinder = VariableBinder.builder() | ||
34 | .parameterList(polarity.isPositive(), parameters, arguments) | ||
35 | .build(); | ||
33 | } | 36 | } |
34 | 37 | ||
35 | public CallPolarity getPolarity() { | 38 | public CallPolarity getPolarity() { |
@@ -37,8 +40,8 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate< | |||
37 | } | 40 | } |
38 | 41 | ||
39 | @Override | 42 | @Override |
40 | public Set<Variable> getBoundVariables() { | 43 | public VariableBinder getVariableBinder() { |
41 | return polarity.isPositive() ? Set.copyOf(getArguments()) : Set.of(); | 44 | return variableBinder; |
42 | } | 45 | } |
43 | 46 | ||
44 | @Override | 47 | @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 fa7979d1..7466cb1d 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 | |||
@@ -8,14 +8,31 @@ 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.substitution.Substitution; | 9 | import tools.refinery.store.query.substitution.Substitution; |
10 | import tools.refinery.store.query.term.NodeVariable; | 10 | import tools.refinery.store.query.term.NodeVariable; |
11 | import tools.refinery.store.query.term.Variable; | ||
12 | 11 | ||
13 | import java.util.Set; | 12 | import java.util.Objects; |
13 | |||
14 | public final class ConstantLiteral implements Literal { | ||
15 | private final NodeVariable variable; | ||
16 | private final int nodeId; | ||
17 | private final VariableBinder variableBinder; | ||
18 | |||
19 | public ConstantLiteral(NodeVariable variable, int nodeId) { | ||
20 | this.variable = variable; | ||
21 | this.nodeId = nodeId; | ||
22 | variableBinder = VariableBinder.builder().variable(variable, VariableDirection.IN_OUT).build(); | ||
23 | } | ||
24 | |||
25 | public NodeVariable getVariable() { | ||
26 | return variable; | ||
27 | } | ||
28 | |||
29 | public int getNodeId() { | ||
30 | return nodeId; | ||
31 | } | ||
14 | 32 | ||
15 | public record ConstantLiteral(NodeVariable variable, int nodeId) implements Literal { | ||
16 | @Override | 33 | @Override |
17 | public Set<Variable> getBoundVariables() { | 34 | public VariableBinder getVariableBinder() { |
18 | return Set.of(variable); | 35 | return variableBinder; |
19 | } | 36 | } |
20 | 37 | ||
21 | @Override | 38 | @Override |
@@ -32,8 +49,23 @@ public record ConstantLiteral(NodeVariable variable, int nodeId) implements Lite | |||
32 | return helper.variableEqual(variable, otherConstantLiteral.variable) && nodeId == otherConstantLiteral.nodeId; | 49 | return helper.variableEqual(variable, otherConstantLiteral.variable) && nodeId == otherConstantLiteral.nodeId; |
33 | } | 50 | } |
34 | 51 | ||
52 | |||
35 | @Override | 53 | @Override |
36 | public String toString() { | 54 | public String toString() { |
37 | return "%s === @Constant %d".formatted(variable, nodeId); | 55 | return "%s === @Constant %d".formatted(variable, nodeId); |
38 | } | 56 | } |
57 | |||
58 | @Override | ||
59 | public boolean equals(Object obj) { | ||
60 | if (obj == this) return true; | ||
61 | if (obj == null || obj.getClass() != this.getClass()) return false; | ||
62 | var that = (ConstantLiteral) obj; | ||
63 | return Objects.equals(this.variable, that.variable) && | ||
64 | this.nodeId == that.nodeId; | ||
65 | } | ||
66 | |||
67 | @Override | ||
68 | public int hashCode() { | ||
69 | return Objects.hash(getClass(), variable, nodeId); | ||
70 | } | ||
39 | } | 71 | } |
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 11f78fa8..a602d982 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 | |||
@@ -13,10 +13,10 @@ import tools.refinery.store.query.term.Variable; | |||
13 | 13 | ||
14 | import java.util.List; | 14 | import java.util.List; |
15 | import java.util.Objects; | 15 | import java.util.Objects; |
16 | import java.util.Set; | ||
17 | 16 | ||
18 | public class CountLiteral extends AbstractCallLiteral { | 17 | public class CountLiteral extends AbstractCallLiteral { |
19 | private final DataVariable<Integer> resultVariable; | 18 | private final DataVariable<Integer> resultVariable; |
19 | private final VariableBinder variableBinder; | ||
20 | 20 | ||
21 | public CountLiteral(DataVariable<Integer> resultVariable, Constraint target, List<Variable> arguments) { | 21 | public CountLiteral(DataVariable<Integer> resultVariable, Constraint target, List<Variable> arguments) { |
22 | super(target, arguments); | 22 | super(target, arguments); |
@@ -29,6 +29,10 @@ public class CountLiteral extends AbstractCallLiteral { | |||
29 | .formatted(resultVariable)); | 29 | .formatted(resultVariable)); |
30 | } | 30 | } |
31 | this.resultVariable = resultVariable; | 31 | this.resultVariable = resultVariable; |
32 | variableBinder = VariableBinder.builder() | ||
33 | .variable(resultVariable, VariableDirection.OUT) | ||
34 | .parameterList(false, target.getParameters(), arguments) | ||
35 | .build(); | ||
32 | } | 36 | } |
33 | 37 | ||
34 | public DataVariable<Integer> getResultVariable() { | 38 | public DataVariable<Integer> getResultVariable() { |
@@ -36,8 +40,8 @@ public class CountLiteral extends AbstractCallLiteral { | |||
36 | } | 40 | } |
37 | 41 | ||
38 | @Override | 42 | @Override |
39 | public Set<Variable> getBoundVariables() { | 43 | public VariableBinder getVariableBinder() { |
40 | return Set.of(resultVariable); | 44 | return variableBinder; |
41 | } | 45 | } |
42 | 46 | ||
43 | @Override | 47 | @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 3876574c..794cee0d 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 | |||
@@ -5,20 +5,44 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.query.literal; | 6 | package tools.refinery.store.query.literal; |
7 | 7 | ||
8 | import tools.refinery.store.query.term.NodeVariable; | ||
9 | import tools.refinery.store.query.term.Variable; | ||
10 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | 8 | import tools.refinery.store.query.equality.LiteralEqualityHelper; |
11 | import tools.refinery.store.query.substitution.Substitution; | 9 | import tools.refinery.store.query.substitution.Substitution; |
10 | import tools.refinery.store.query.term.NodeVariable; | ||
12 | 11 | ||
13 | import java.util.Set; | 12 | import java.util.Objects; |
14 | 13 | ||
15 | public record EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right) | 14 | public final class EquivalenceLiteral |
16 | implements CanNegate<EquivalenceLiteral> { | 15 | implements CanNegate<EquivalenceLiteral> { |
16 | private final boolean positive; | ||
17 | private final NodeVariable left; | ||
18 | private final NodeVariable right; | ||
19 | private final VariableBinder variableBinder; | ||
20 | |||
21 | public EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right) { | ||
22 | this.positive = positive; | ||
23 | this.left = left; | ||
24 | this.right = right; | ||
25 | variableBinder = VariableBinder.builder() | ||
26 | .variable(left, positive ? VariableDirection.IN_OUT : VariableDirection.IN) | ||
27 | .variable(right, VariableDirection.IN) | ||
28 | .build(); | ||
29 | } | ||
30 | |||
31 | public boolean isPositive() { | ||
32 | return positive; | ||
33 | } | ||
34 | |||
35 | public NodeVariable getLeft() { | ||
36 | return left; | ||
37 | } | ||
38 | |||
39 | public NodeVariable getRight() { | ||
40 | return right; | ||
41 | } | ||
42 | |||
17 | @Override | 43 | @Override |
18 | public Set<Variable> getBoundVariables() { | 44 | public VariableBinder getVariableBinder() { |
19 | // If one side of a {@code positive} equivalence is bound, it may bind its other side, but we under-approximate | 45 | return variableBinder; |
20 | // this behavior by not binding any of the sides by default. | ||
21 | return Set.of(); | ||
22 | } | 46 | } |
23 | 47 | ||
24 | @Override | 48 | @Override |
@@ -54,4 +78,19 @@ public record EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariab | |||
54 | public String toString() { | 78 | public String toString() { |
55 | return "%s %s %s".formatted(left, positive ? "===" : "!==", right); | 79 | return "%s %s %s".formatted(left, positive ? "===" : "!==", right); |
56 | } | 80 | } |
81 | |||
82 | @Override | ||
83 | public boolean equals(Object obj) { | ||
84 | if (obj == this) return true; | ||
85 | if (obj == null || obj.getClass() != this.getClass()) return false; | ||
86 | var that = (EquivalenceLiteral) obj; | ||
87 | return this.positive == that.positive && | ||
88 | Objects.equals(this.left, that.left) && | ||
89 | Objects.equals(this.right, that.right); | ||
90 | } | ||
91 | |||
92 | @Override | ||
93 | public int hashCode() { | ||
94 | return Objects.hash(getClass(), positive, left, right); | ||
95 | } | ||
57 | } | 96 | } |
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 52411ee8..c3c111a4 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 | |||
@@ -5,14 +5,11 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.query.literal; | 6 | package tools.refinery.store.query.literal; |
7 | 7 | ||
8 | import tools.refinery.store.query.term.Variable; | ||
9 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | 8 | import tools.refinery.store.query.equality.LiteralEqualityHelper; |
10 | import tools.refinery.store.query.substitution.Substitution; | 9 | import tools.refinery.store.query.substitution.Substitution; |
11 | 10 | ||
12 | import java.util.Set; | ||
13 | |||
14 | public interface Literal { | 11 | public interface Literal { |
15 | Set<Variable> getBoundVariables(); | 12 | VariableBinder getVariableBinder(); |
16 | 13 | ||
17 | Literal substitute(Substitution substitution); | 14 | Literal substitute(Substitution substitution); |
18 | 15 | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java new file mode 100644 index 00000000..5f43d07d --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java | |||
@@ -0,0 +1,64 @@ | |||
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.term.Variable; | ||
9 | |||
10 | import java.util.Map; | ||
11 | import java.util.Set; | ||
12 | import java.util.stream.Stream; | ||
13 | |||
14 | public final class VariableBinder { | ||
15 | public static final VariableBinder EMPTY = new VariableBinder(Map.of()); | ||
16 | |||
17 | private final Map<Variable, VariableDirection> directionMap; | ||
18 | |||
19 | VariableBinder(Map<Variable, VariableDirection> directionMap) { | ||
20 | this.directionMap = directionMap; | ||
21 | } | ||
22 | |||
23 | public VariableDirection getDirection(Variable variable) { | ||
24 | var direction = directionMap.get(variable); | ||
25 | if (direction == null) { | ||
26 | throw new IllegalArgumentException("No such variable " + variable); | ||
27 | } | ||
28 | return direction; | ||
29 | } | ||
30 | |||
31 | public VariableDirection getDirection(Variable variable, Set<? extends Variable> positiveVariables) { | ||
32 | var direction = getDirection(variable); | ||
33 | return disambiguateDirection(direction, variable, positiveVariables); | ||
34 | } | ||
35 | |||
36 | public Stream<Variable> getVariablesWithDirection(VariableDirection direction) { | ||
37 | return directionMap.entrySet().stream() | ||
38 | .filter(pair -> pair.getValue() == direction) | ||
39 | .map(Map.Entry::getKey); | ||
40 | } | ||
41 | |||
42 | public Stream<Variable> getVariablesWithDirection(VariableDirection direction, | ||
43 | Set<? extends Variable> positiveVariables) { | ||
44 | if (direction == VariableDirection.NEGATIVE) { | ||
45 | throw new IllegalArgumentException("Use #getVariablesWithDirection(VariableDirection) if disambiguation " + | ||
46 | "of VariableDirection#NEGATIVE variables according to the containing DnfClose is not desired"); | ||
47 | } | ||
48 | return directionMap.entrySet().stream() | ||
49 | .filter(pair -> disambiguateDirection(pair.getValue(), pair.getKey(), positiveVariables) == direction) | ||
50 | .map(Map.Entry::getKey); | ||
51 | } | ||
52 | |||
53 | private VariableDirection disambiguateDirection(VariableDirection direction, Variable variable, | ||
54 | Set<? extends Variable> positiveVariables) { | ||
55 | if (direction != VariableDirection.NEGATIVE) { | ||
56 | return direction; | ||
57 | } | ||
58 | return positiveVariables.contains(variable) ? VariableDirection.IN : VariableDirection.CLOSURE; | ||
59 | } | ||
60 | |||
61 | public static VariableBinderBuilder builder() { | ||
62 | return new VariableBinderBuilder(); | ||
63 | } | ||
64 | } | ||
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 new file mode 100644 index 00000000..b0d47240 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java | |||
@@ -0,0 +1,96 @@ | |||
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/VariableDirection.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java new file mode 100644 index 00000000..444dcbbf --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java | |||
@@ -0,0 +1,101 @@ | |||
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.ParameterDirection; | ||
10 | |||
11 | public enum VariableDirection { | ||
12 | /** | ||
13 | * Binds a node variable or check equality with a node variable. | ||
14 | * <p> | ||
15 | * This is the usual direction for positive constraints on nodes. A data variable may have multiple {@code InOut} | ||
16 | * bindings, even on the same parameter list. | ||
17 | * <p> | ||
18 | * Cannot be used for data variables. | ||
19 | */ | ||
20 | IN_OUT("@InOut"), | ||
21 | |||
22 | /** | ||
23 | * Binds a data variable. | ||
24 | * <p> | ||
25 | * 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. | ||
27 | * <p> | ||
28 | * Cannot be used for node variables. | ||
29 | */ | ||
30 | OUT("@Out"), | ||
31 | |||
32 | /** | ||
33 | * Either takes a bound data variable or enumerates all possible data variable bindings. | ||
34 | * <p> | ||
35 | * Cannot be used for data variables. | ||
36 | */ | ||
37 | NEGATIVE("@Negative"), | ||
38 | |||
39 | /** | ||
40 | * Takes an already bound variable. | ||
41 | * <p> | ||
42 | * May be used with node or data variables. An {@code @InOut} or {@code @Out} binding on the same parameter list | ||
43 | * cannot satisfy the {@code @In} binding, because it might introduce a (non-monotonic) circular dependency. | ||
44 | */ | ||
45 | IN("@In"), | ||
46 | |||
47 | /** | ||
48 | * Enumerates over all possible data variable bindings. | ||
49 | * <p> | ||
50 | * May be used with node or data variables. The variable may not appear in any other parameter list. A data | ||
51 | * variable may only appear once in the parameter list, but node variables can appear multiple times to form | ||
52 | * diagonal constraints. | ||
53 | */ | ||
54 | CLOSURE("@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 | |||
94 | public static VariableDirection from(boolean positive, ParameterDirection parameterDirection) { | ||
95 | return switch (parameterDirection) { | ||
96 | case IN_OUT -> positive ? IN_OUT : NEGATIVE; | ||
97 | case OUT -> positive ? OUT : CLOSURE; | ||
98 | case IN -> IN; | ||
99 | }; | ||
100 | } | ||
101 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/SubstitutionBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/SubstitutionBuilder.java index 658a26e3..37fb6908 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/SubstitutionBuilder.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/SubstitutionBuilder.java | |||
@@ -32,9 +32,10 @@ public class SubstitutionBuilder { | |||
32 | } | 32 | } |
33 | 33 | ||
34 | public SubstitutionBuilder putChecked(Variable original, Variable substitute) { | 34 | public SubstitutionBuilder putChecked(Variable original, Variable substitute) { |
35 | if (!original.getSort().equals(substitute.getSort())) { | 35 | if (!original.tryGetType().equals(substitute.tryGetType())) { |
36 | throw new IllegalArgumentException("Cannot substitute variable %s of sort %s with variable %s of sort %s" | 36 | throw new IllegalArgumentException("Cannot substitute variable %s of sort %s with variable %s of sort %s" |
37 | .formatted(original, original.getSort(), substitute, substitute.getSort())); | 37 | .formatted(original, original.tryGetType().map(Class::getName).orElse("node"), substitute, |
38 | substitute.tryGetType().map(Class::getName).orElse("node"))); | ||
38 | } | 39 | } |
39 | if (map.containsKey(original)) { | 40 | if (map.containsKey(original)) { |
40 | throw new IllegalArgumentException("Already has substitution for variable %s".formatted(original)); | 41 | throw new IllegalArgumentException("Already has substitution for variable %s".formatted(original)); |
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 ccc063af..5864ee56 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 | |||
@@ -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 | 10 | ||
11 | import java.util.Optional; | ||
11 | import java.util.Set; | 12 | import java.util.Set; |
12 | 13 | ||
13 | public abstract sealed class AnyDataVariable extends Variable implements AnyTerm permits DataVariable { | 14 | public abstract sealed class AnyDataVariable extends Variable implements AnyTerm permits DataVariable { |
@@ -16,6 +17,11 @@ public abstract sealed class AnyDataVariable extends Variable implements AnyTerm | |||
16 | } | 17 | } |
17 | 18 | ||
18 | @Override | 19 | @Override |
20 | public Optional<Class<?>> tryGetType() { | ||
21 | return Optional.of(getType()); | ||
22 | } | ||
23 | |||
24 | @Override | ||
19 | public NodeVariable asNodeVariable() { | 25 | public NodeVariable asNodeVariable() { |
20 | throw new IllegalStateException("%s is a data variable".formatted(this)); | 26 | throw new IllegalStateException("%s is a data variable".formatted(this)); |
21 | } | 27 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataSort.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataSort.java deleted file mode 100644 index 6b8669ee..00000000 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataSort.java +++ /dev/null | |||
@@ -1,34 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.query.term; | ||
7 | |||
8 | import org.jetbrains.annotations.Nullable; | ||
9 | |||
10 | public record DataSort<T>(Class<T> type) implements Sort { | ||
11 | public static final DataSort<Integer> INT = new DataSort<>(Integer.class); | ||
12 | |||
13 | public static final DataSort<Boolean> BOOL = new DataSort<>(Boolean.class); | ||
14 | |||
15 | @Override | ||
16 | public boolean isInstance(Variable variable) { | ||
17 | return variable instanceof DataVariable<?> dataVariable && type.equals(dataVariable.getType()); | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public DataVariable<T> newInstance(@Nullable String name) { | ||
22 | return Variable.of(name, type); | ||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public DataVariable<T> newInstance() { | ||
27 | return newInstance(null); | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public String toString() { | ||
32 | return type.getName(); | ||
33 | } | ||
34 | } | ||
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 db160f68..00950360 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 | |||
@@ -22,11 +22,6 @@ public final class DataVariable<T> extends AnyDataVariable implements Term<T> { | |||
22 | } | 22 | } |
23 | 23 | ||
24 | @Override | 24 | @Override |
25 | public DataSort<T> getSort() { | ||
26 | return new DataSort<>(getType()); | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | public Class<T> getType() { | 25 | public Class<T> getType() { |
31 | return type; | 26 | return type; |
32 | } | 27 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeSort.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeSort.java deleted file mode 100644 index b9be03f7..00000000 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeSort.java +++ /dev/null | |||
@@ -1,35 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.query.term; | ||
7 | |||
8 | import org.jetbrains.annotations.Nullable; | ||
9 | |||
10 | public final class NodeSort implements Sort { | ||
11 | public static final NodeSort INSTANCE = new NodeSort(); | ||
12 | |||
13 | private NodeSort() { | ||
14 | } | ||
15 | |||
16 | @Override | ||
17 | public boolean isInstance(Variable variable) { | ||
18 | return variable instanceof NodeVariable; | ||
19 | } | ||
20 | |||
21 | @Override | ||
22 | public NodeVariable newInstance(@Nullable String name) { | ||
23 | return new NodeVariable(name); | ||
24 | } | ||
25 | |||
26 | @Override | ||
27 | public NodeVariable newInstance() { | ||
28 | return newInstance(null); | ||
29 | } | ||
30 | |||
31 | @Override | ||
32 | public String toString() { | ||
33 | return "<node>"; | ||
34 | } | ||
35 | } | ||
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 de2f945a..37f9d477 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 | |||
@@ -9,14 +9,16 @@ import org.jetbrains.annotations.Nullable; | |||
9 | import tools.refinery.store.query.literal.ConstantLiteral; | 9 | import tools.refinery.store.query.literal.ConstantLiteral; |
10 | import tools.refinery.store.query.literal.EquivalenceLiteral; | 10 | import tools.refinery.store.query.literal.EquivalenceLiteral; |
11 | 11 | ||
12 | import java.util.Optional; | ||
13 | |||
12 | public final class NodeVariable extends Variable { | 14 | public final class NodeVariable extends Variable { |
13 | NodeVariable(@Nullable String name) { | 15 | NodeVariable(@Nullable String name) { |
14 | super(name); | 16 | super(name); |
15 | } | 17 | } |
16 | 18 | ||
17 | @Override | 19 | @Override |
18 | public NodeSort getSort() { | 20 | public Optional<Class<?>> tryGetType() { |
19 | return NodeSort.INSTANCE; | 21 | return Optional.empty(); |
20 | } | 22 | } |
21 | 23 | ||
22 | @Override | 24 | @Override |
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 new file mode 100644 index 00000000..29aedbef --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Parameter.java | |||
@@ -0,0 +1,63 @@ | |||
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.term; | ||
7 | |||
8 | import java.util.Objects; | ||
9 | import java.util.Optional; | ||
10 | |||
11 | public class Parameter { | ||
12 | public static final Parameter NODE_IN_OUT = new Parameter(null, ParameterDirection.IN_OUT); | ||
13 | |||
14 | private final Class<?> dataType; | ||
15 | private final ParameterDirection direction; | ||
16 | |||
17 | public Parameter(Class<?> dataType, ParameterDirection direction) { | ||
18 | this.dataType = dataType; | ||
19 | this.direction = direction; | ||
20 | if (isDataVariable()) { | ||
21 | if (direction == ParameterDirection.IN_OUT) { | ||
22 | throw new IllegalArgumentException("IN_OUT direction is not supported for data parameters"); | ||
23 | } | ||
24 | } else if (direction == ParameterDirection.OUT) { | ||
25 | throw new IllegalArgumentException("OUT direction is not supported for node parameters"); | ||
26 | } | ||
27 | } | ||
28 | |||
29 | public boolean isDataVariable() { | ||
30 | return dataType != null; | ||
31 | } | ||
32 | |||
33 | public Optional<Class<?>> tryGetType() { | ||
34 | return Optional.ofNullable(dataType); | ||
35 | } | ||
36 | |||
37 | public ParameterDirection getDirection() { | ||
38 | return direction; | ||
39 | } | ||
40 | |||
41 | public boolean isAssignable(Variable variable) { | ||
42 | if (variable instanceof AnyDataVariable dataVariable) { | ||
43 | return dataVariable.getType().equals(dataType); | ||
44 | } else if (variable instanceof NodeVariable) { | ||
45 | return !isDataVariable(); | ||
46 | } else { | ||
47 | throw new IllegalArgumentException("Unknown variable " + variable); | ||
48 | } | ||
49 | } | ||
50 | |||
51 | @Override | ||
52 | public boolean equals(Object o) { | ||
53 | if (this == o) return true; | ||
54 | if (o == null || getClass() != o.getClass()) return false; | ||
55 | Parameter parameter = (Parameter) o; | ||
56 | return Objects.equals(dataType, parameter.dataType) && direction == parameter.direction; | ||
57 | } | ||
58 | |||
59 | @Override | ||
60 | public int hashCode() { | ||
61 | return Objects.hash(dataType, direction); | ||
62 | } | ||
63 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ParameterDirection.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ParameterDirection.java new file mode 100644 index 00000000..652208aa --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ParameterDirection.java | |||
@@ -0,0 +1,23 @@ | |||
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.term; | ||
7 | |||
8 | public enum ParameterDirection { | ||
9 | IN_OUT("@InOut"), | ||
10 | OUT("@Out"), | ||
11 | IN("@In"); | ||
12 | |||
13 | private final String name; | ||
14 | |||
15 | ParameterDirection(String name) { | ||
16 | this.name = name; | ||
17 | } | ||
18 | |||
19 | @Override | ||
20 | public String toString() { | ||
21 | return name; | ||
22 | } | ||
23 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Sort.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Sort.java deleted file mode 100644 index 2b3345f9..00000000 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Sort.java +++ /dev/null | |||
@@ -1,16 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.query.term; | ||
7 | |||
8 | import org.jetbrains.annotations.Nullable; | ||
9 | |||
10 | public sealed interface Sort permits DataSort, NodeSort { | ||
11 | boolean isInstance(Variable variable); | ||
12 | |||
13 | Variable newInstance(@Nullable String name); | ||
14 | |||
15 | Variable newInstance(); | ||
16 | } | ||
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 c4ca6f77..869120fa 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 | |||
@@ -9,6 +9,7 @@ import org.jetbrains.annotations.Nullable; | |||
9 | import tools.refinery.store.query.dnf.DnfUtils; | 9 | import tools.refinery.store.query.dnf.DnfUtils; |
10 | 10 | ||
11 | import java.util.Objects; | 11 | import java.util.Objects; |
12 | import java.util.Optional; | ||
12 | 13 | ||
13 | public abstract sealed class Variable permits AnyDataVariable, NodeVariable { | 14 | public abstract sealed class Variable permits AnyDataVariable, NodeVariable { |
14 | private final String explicitName; | 15 | private final String explicitName; |
@@ -19,7 +20,7 @@ public abstract sealed class Variable permits AnyDataVariable, NodeVariable { | |||
19 | uniqueName = DnfUtils.generateUniqueName(name); | 20 | uniqueName = DnfUtils.generateUniqueName(name); |
20 | } | 21 | } |
21 | 22 | ||
22 | public abstract Sort getSort(); | 23 | public abstract Optional<Class<?>> tryGetType(); |
23 | 24 | ||
24 | public String getName() { | 25 | public String getName() { |
25 | return explicitName == null ? uniqueName : explicitName; | 26 | return explicitName == null ? uniqueName : explicitName; |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AbstractFunctionView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AbstractFunctionView.java index c0aa35bf..c6f3dd43 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AbstractFunctionView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AbstractFunctionView.java | |||
@@ -7,12 +7,12 @@ package tools.refinery.store.query.view; | |||
7 | 7 | ||
8 | import tools.refinery.store.model.Model; | 8 | import tools.refinery.store.model.Model; |
9 | import tools.refinery.store.query.dnf.FunctionalDependency; | 9 | import tools.refinery.store.query.dnf.FunctionalDependency; |
10 | import tools.refinery.store.query.term.NodeSort; | 10 | import tools.refinery.store.query.term.Parameter; |
11 | import tools.refinery.store.query.term.Sort; | ||
12 | import tools.refinery.store.representation.Symbol; | 11 | import tools.refinery.store.representation.Symbol; |
13 | import tools.refinery.store.tuple.Tuple; | 12 | import tools.refinery.store.tuple.Tuple; |
14 | import tools.refinery.store.tuple.Tuple1; | 13 | import tools.refinery.store.tuple.Tuple1; |
15 | 14 | ||
15 | import java.util.Arrays; | ||
16 | import java.util.List; | 16 | import java.util.List; |
17 | import java.util.Objects; | 17 | import java.util.Objects; |
18 | import java.util.Set; | 18 | import java.util.Set; |
@@ -21,10 +21,12 @@ import java.util.stream.IntStream; | |||
21 | 21 | ||
22 | public abstract class AbstractFunctionView<T> extends SymbolView<T> { | 22 | public abstract class AbstractFunctionView<T> extends SymbolView<T> { |
23 | private final T defaultValue; | 23 | private final T defaultValue; |
24 | private final List<Parameter> parameters; | ||
24 | 25 | ||
25 | protected AbstractFunctionView(Symbol<T> symbol, String name) { | 26 | protected AbstractFunctionView(Symbol<T> symbol, String name, Parameter outParameter) { |
26 | super(symbol, name); | 27 | super(symbol, name); |
27 | defaultValue = symbol.defaultValue(); | 28 | defaultValue = symbol.defaultValue(); |
29 | parameters = createParameters(symbol.arity(), outParameter); | ||
28 | } | 30 | } |
29 | 31 | ||
30 | @Override | 32 | @Override |
@@ -48,8 +50,6 @@ public abstract class AbstractFunctionView<T> extends SymbolView<T> { | |||
48 | return !Objects.equals(defaultValue, value); | 50 | return !Objects.equals(defaultValue, value); |
49 | } | 51 | } |
50 | 52 | ||
51 | protected abstract Sort getForwardMappedValueSort(); | ||
52 | |||
53 | protected Object forwardMapValue(Tuple key, T value) { | 53 | protected Object forwardMapValue(Tuple key, T value) { |
54 | return value; | 54 | return value; |
55 | } | 55 | } |
@@ -85,19 +85,8 @@ public abstract class AbstractFunctionView<T> extends SymbolView<T> { | |||
85 | } | 85 | } |
86 | 86 | ||
87 | @Override | 87 | @Override |
88 | public int arity() { | 88 | public List<Parameter> getParameters() { |
89 | return getSymbol().arity() + 1; | 89 | return parameters; |
90 | } | ||
91 | |||
92 | @Override | ||
93 | public List<Sort> getSorts() { | ||
94 | var sorts = new Sort[arity()]; | ||
95 | int valueIndex = sorts.length - 1; | ||
96 | for (int i = 0; i < valueIndex; i++) { | ||
97 | sorts[i] = NodeSort.INSTANCE; | ||
98 | } | ||
99 | sorts[valueIndex] = getForwardMappedValueSort(); | ||
100 | return List.of(sorts); | ||
101 | } | 90 | } |
102 | 91 | ||
103 | @Override | 92 | @Override |
@@ -106,11 +95,18 @@ public abstract class AbstractFunctionView<T> extends SymbolView<T> { | |||
106 | if (o == null || getClass() != o.getClass()) return false; | 95 | if (o == null || getClass() != o.getClass()) return false; |
107 | if (!super.equals(o)) return false; | 96 | if (!super.equals(o)) return false; |
108 | AbstractFunctionView<?> that = (AbstractFunctionView<?>) o; | 97 | AbstractFunctionView<?> that = (AbstractFunctionView<?>) o; |
109 | return Objects.equals(defaultValue, that.defaultValue); | 98 | return Objects.equals(defaultValue, that.defaultValue) && Objects.equals(parameters, that.parameters); |
110 | } | 99 | } |
111 | 100 | ||
112 | @Override | 101 | @Override |
113 | public int hashCode() { | 102 | public int hashCode() { |
114 | return Objects.hash(super.hashCode(), defaultValue); | 103 | return Objects.hash(super.hashCode(), defaultValue, parameters); |
104 | } | ||
105 | |||
106 | private static List<Parameter> createParameters(int symbolArity, Parameter outParameter) { | ||
107 | var parameters = new Parameter[symbolArity + 1]; | ||
108 | Arrays.fill(parameters, Parameter.NODE_IN_OUT); | ||
109 | parameters[symbolArity] = outParameter; | ||
110 | return List.of(parameters); | ||
115 | } | 111 | } |
116 | } | 112 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionView.java index cf946d54..1b89e77c 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionView.java | |||
@@ -5,21 +5,16 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.query.view; | 6 | package tools.refinery.store.query.view; |
7 | 7 | ||
8 | import tools.refinery.store.query.term.DataSort; | 8 | import tools.refinery.store.query.term.Parameter; |
9 | import tools.refinery.store.query.term.Sort; | 9 | import tools.refinery.store.query.term.ParameterDirection; |
10 | import tools.refinery.store.representation.Symbol; | 10 | import tools.refinery.store.representation.Symbol; |
11 | 11 | ||
12 | public final class FunctionView<T> extends AbstractFunctionView<T> { | 12 | public final class FunctionView<T> extends AbstractFunctionView<T> { |
13 | public FunctionView(Symbol<T> symbol, String name) { | 13 | public FunctionView(Symbol<T> symbol, String name) { |
14 | super(symbol, name); | 14 | super(symbol, name, new Parameter(symbol.valueType(), ParameterDirection.OUT)); |
15 | } | 15 | } |
16 | 16 | ||
17 | public FunctionView(Symbol<T> symbol) { | 17 | public FunctionView(Symbol<T> symbol) { |
18 | this(symbol, "function"); | 18 | this(symbol, "function"); |
19 | } | 19 | } |
20 | |||
21 | @Override | ||
22 | protected Sort getForwardMappedValueSort() { | ||
23 | return new DataSort<>(getSymbol().valueType()); | ||
24 | } | ||
25 | } | 20 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/NodeFunctionView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/NodeFunctionView.java index 73c296e0..e9785c67 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/NodeFunctionView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/NodeFunctionView.java | |||
@@ -5,22 +5,16 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.query.view; | 6 | package tools.refinery.store.query.view; |
7 | 7 | ||
8 | import tools.refinery.store.query.term.NodeSort; | 8 | import tools.refinery.store.query.term.Parameter; |
9 | import tools.refinery.store.query.term.Sort; | ||
10 | import tools.refinery.store.representation.Symbol; | 9 | import tools.refinery.store.representation.Symbol; |
11 | import tools.refinery.store.tuple.Tuple1; | 10 | import tools.refinery.store.tuple.Tuple1; |
12 | 11 | ||
13 | public final class NodeFunctionView extends AbstractFunctionView<Tuple1> { | 12 | public final class NodeFunctionView extends AbstractFunctionView<Tuple1> { |
14 | public NodeFunctionView(Symbol<Tuple1> symbol, String name) { | 13 | public NodeFunctionView(Symbol<Tuple1> symbol, String name) { |
15 | super(symbol, name); | 14 | super(symbol, name, Parameter.NODE_IN_OUT); |
16 | } | 15 | } |
17 | 16 | ||
18 | public NodeFunctionView(Symbol<Tuple1> symbol) { | 17 | public NodeFunctionView(Symbol<Tuple1> symbol) { |
19 | this(symbol, "function"); | 18 | this(symbol, "function"); |
20 | } | 19 | } |
21 | |||
22 | @Override | ||
23 | protected Sort getForwardMappedValueSort() { | ||
24 | return NodeSort.INSTANCE; | ||
25 | } | ||
26 | } | 20 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingView.java index 19862e3a..7e5b7788 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingView.java | |||
@@ -6,22 +6,26 @@ | |||
6 | package tools.refinery.store.query.view; | 6 | package tools.refinery.store.query.view; |
7 | 7 | ||
8 | import tools.refinery.store.model.Model; | 8 | import tools.refinery.store.model.Model; |
9 | import tools.refinery.store.query.term.NodeSort; | 9 | import tools.refinery.store.query.term.Parameter; |
10 | import tools.refinery.store.query.term.Sort; | 10 | import tools.refinery.store.representation.Symbol; |
11 | import tools.refinery.store.tuple.Tuple; | 11 | import tools.refinery.store.tuple.Tuple; |
12 | import tools.refinery.store.tuple.Tuple1; | 12 | import tools.refinery.store.tuple.Tuple1; |
13 | import tools.refinery.store.representation.Symbol; | ||
14 | 13 | ||
15 | import java.util.Arrays; | 14 | import java.util.Arrays; |
16 | import java.util.List; | 15 | import java.util.List; |
16 | import java.util.Objects; | ||
17 | 17 | ||
18 | public abstract class TuplePreservingView<T> extends SymbolView<T> { | 18 | public abstract class TuplePreservingView<T> extends SymbolView<T> { |
19 | private final List<Parameter> parameters; | ||
20 | |||
19 | protected TuplePreservingView(Symbol<T> symbol, String name) { | 21 | protected TuplePreservingView(Symbol<T> symbol, String name) { |
20 | super(symbol, name); | 22 | super(symbol, name); |
23 | this.parameters = createParameters(symbol.arity()); | ||
21 | } | 24 | } |
22 | 25 | ||
23 | protected TuplePreservingView(Symbol<T> symbol) { | 26 | protected TuplePreservingView(Symbol<T> symbol) { |
24 | super(symbol); | 27 | super(symbol); |
28 | this.parameters = createParameters(symbol.arity()); | ||
25 | } | 29 | } |
26 | 30 | ||
27 | public Object[] forwardMap(Tuple key) { | 31 | public Object[] forwardMap(Tuple key) { |
@@ -52,14 +56,27 @@ public abstract class TuplePreservingView<T> extends SymbolView<T> { | |||
52 | } | 56 | } |
53 | 57 | ||
54 | @Override | 58 | @Override |
55 | public int arity() { | 59 | public List<Parameter> getParameters() { |
56 | return this.getSymbol().arity(); | 60 | return parameters; |
61 | } | ||
62 | |||
63 | @Override | ||
64 | public boolean equals(Object o) { | ||
65 | if (this == o) return true; | ||
66 | if (o == null || getClass() != o.getClass()) return false; | ||
67 | if (!super.equals(o)) return false; | ||
68 | TuplePreservingView<?> that = (TuplePreservingView<?>) o; | ||
69 | return Objects.equals(parameters, that.parameters); | ||
57 | } | 70 | } |
58 | 71 | ||
59 | @Override | 72 | @Override |
60 | public List<Sort> getSorts() { | 73 | public int hashCode() { |
61 | var sorts = new Sort[arity()]; | 74 | return Objects.hash(super.hashCode(), parameters); |
62 | Arrays.fill(sorts, NodeSort.INSTANCE); | 75 | } |
63 | return List.of(sorts); | 76 | |
77 | private static List<Parameter> createParameters(int arity) { | ||
78 | var parameters = new Parameter[arity]; | ||
79 | Arrays.fill(parameters, Parameter.NODE_IN_OUT); | ||
80 | return List.of(parameters); | ||
64 | } | 81 | } |
65 | } | 82 | } |
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java index 01e2ccf6..4edea401 100644 --- a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderLiteralEliminationTest.java | |||
@@ -3,31 +3,36 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.query; | 6 | package tools.refinery.store.query.dnf; |
7 | 7 | ||
8 | import org.junit.jupiter.api.Test; | 8 | import org.junit.jupiter.api.Test; |
9 | import org.junit.jupiter.params.ParameterizedTest; | 9 | import org.junit.jupiter.params.ParameterizedTest; |
10 | import org.junit.jupiter.params.provider.CsvSource; | 10 | import org.junit.jupiter.params.provider.CsvSource; |
11 | import tools.refinery.store.query.dnf.Dnf; | ||
12 | import tools.refinery.store.query.literal.BooleanLiteral; | 11 | import tools.refinery.store.query.literal.BooleanLiteral; |
12 | import tools.refinery.store.query.term.NodeVariable; | ||
13 | import tools.refinery.store.query.term.Variable; | 13 | import tools.refinery.store.query.term.Variable; |
14 | import tools.refinery.store.query.term.bool.BoolTerms; | 14 | import tools.refinery.store.query.term.bool.BoolTerms; |
15 | import tools.refinery.store.query.view.KeyOnlyView; | 15 | import tools.refinery.store.query.view.KeyOnlyView; |
16 | import tools.refinery.store.query.view.SymbolView; | ||
16 | import tools.refinery.store.representation.Symbol; | 17 | import tools.refinery.store.representation.Symbol; |
17 | 18 | ||
19 | import java.util.List; | ||
20 | |||
18 | import static org.hamcrest.MatcherAssert.assertThat; | 21 | import static org.hamcrest.MatcherAssert.assertThat; |
19 | import static tools.refinery.store.query.literal.Literals.assume; | 22 | import static tools.refinery.store.query.literal.Literals.assume; |
20 | import static tools.refinery.store.query.literal.Literals.not; | 23 | import static tools.refinery.store.query.literal.Literals.not; |
21 | import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo; | 24 | import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo; |
22 | 25 | ||
23 | class DnfBuilderTest { | 26 | class DnfBuilderLiteralEliminationTest { |
27 | private final Symbol<Boolean> friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
28 | private final SymbolView<Boolean> friendView = new KeyOnlyView<>(friend); | ||
29 | private final NodeVariable p = Variable.of("p"); | ||
30 | private final NodeVariable q = Variable.of("q"); | ||
31 | private final Dnf trueDnf = Dnf.builder().parameter(p).clause().build(); | ||
32 | private final Dnf falseDnf = Dnf.builder().parameter(p).build(); | ||
33 | |||
24 | @Test | 34 | @Test |
25 | void eliminateTrueTest() { | 35 | void eliminateTrueTest() { |
26 | var p = Variable.of("p"); | ||
27 | var q = Variable.of("q"); | ||
28 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
29 | var friendView = new KeyOnlyView<>(friend); | ||
30 | |||
31 | var actual = Dnf.builder() | 36 | var actual = Dnf.builder() |
32 | .parameters(p, q) | 37 | .parameters(p, q) |
33 | .clause(BooleanLiteral.TRUE, friendView.call(p, q)) | 38 | .clause(BooleanLiteral.TRUE, friendView.call(p, q)) |
@@ -39,11 +44,6 @@ class DnfBuilderTest { | |||
39 | 44 | ||
40 | @Test | 45 | @Test |
41 | void eliminateTrueAssumptionTest() { | 46 | void eliminateTrueAssumptionTest() { |
42 | var p = Variable.of("p"); | ||
43 | var q = Variable.of("q"); | ||
44 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
45 | var friendView = new KeyOnlyView<>(friend); | ||
46 | |||
47 | var actual = Dnf.builder() | 47 | var actual = Dnf.builder() |
48 | .parameters(p, q) | 48 | .parameters(p, q) |
49 | .clause(assume(BoolTerms.constant(true)), friendView.call(p, q)) | 49 | .clause(assume(BoolTerms.constant(true)), friendView.call(p, q)) |
@@ -55,11 +55,6 @@ class DnfBuilderTest { | |||
55 | 55 | ||
56 | @Test | 56 | @Test |
57 | void eliminateFalseTest() { | 57 | void eliminateFalseTest() { |
58 | var p = Variable.of("p"); | ||
59 | var q = Variable.of("q"); | ||
60 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
61 | var friendView = new KeyOnlyView<>(friend); | ||
62 | |||
63 | var actual = Dnf.builder() | 58 | var actual = Dnf.builder() |
64 | .parameters(p, q) | 59 | .parameters(p, q) |
65 | .clause(friendView.call(p, q)) | 60 | .clause(friendView.call(p, q)) |
@@ -76,11 +71,6 @@ class DnfBuilderTest { | |||
76 | "null" | 71 | "null" |
77 | }, nullValues = "null") | 72 | }, nullValues = "null") |
78 | void eliminateFalseAssumptionTest(Boolean value) { | 73 | void eliminateFalseAssumptionTest(Boolean value) { |
79 | var p = Variable.of("p"); | ||
80 | var q = Variable.of("q"); | ||
81 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
82 | var friendView = new KeyOnlyView<>(friend); | ||
83 | |||
84 | var actual = Dnf.builder() | 74 | var actual = Dnf.builder() |
85 | .parameters(p, q) | 75 | .parameters(p, q) |
86 | .clause(friendView.call(p, q)) | 76 | .clause(friendView.call(p, q)) |
@@ -93,11 +83,6 @@ class DnfBuilderTest { | |||
93 | 83 | ||
94 | @Test | 84 | @Test |
95 | void alwaysTrueTest() { | 85 | void alwaysTrueTest() { |
96 | var p = Variable.of("p"); | ||
97 | var q = Variable.of("q"); | ||
98 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
99 | var friendView = new KeyOnlyView<>(friend); | ||
100 | |||
101 | var actual = Dnf.builder() | 86 | var actual = Dnf.builder() |
102 | .parameters(p, q) | 87 | .parameters(p, q) |
103 | .clause(friendView.call(p, q)) | 88 | .clause(friendView.call(p, q)) |
@@ -110,11 +95,6 @@ class DnfBuilderTest { | |||
110 | 95 | ||
111 | @Test | 96 | @Test |
112 | void alwaysFalseTest() { | 97 | void alwaysFalseTest() { |
113 | var p = Variable.of("p"); | ||
114 | var q = Variable.of("q"); | ||
115 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
116 | var friendView = new KeyOnlyView<>(friend); | ||
117 | |||
118 | var actual = Dnf.builder() | 98 | var actual = Dnf.builder() |
119 | .parameters(p, q) | 99 | .parameters(p, q) |
120 | .clause(friendView.call(p, q), BooleanLiteral.FALSE) | 100 | .clause(friendView.call(p, q), BooleanLiteral.FALSE) |
@@ -126,12 +106,6 @@ class DnfBuilderTest { | |||
126 | 106 | ||
127 | @Test | 107 | @Test |
128 | void eliminateTrueDnfTest() { | 108 | void eliminateTrueDnfTest() { |
129 | var p = Variable.of("p"); | ||
130 | var q = Variable.of("q"); | ||
131 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
132 | var friendView = new KeyOnlyView<>(friend); | ||
133 | var trueDnf = Dnf.builder().parameter(p).clause().build(); | ||
134 | |||
135 | var actual = Dnf.builder() | 109 | var actual = Dnf.builder() |
136 | .parameters(p, q) | 110 | .parameters(p, q) |
137 | .clause(trueDnf.call(q), friendView.call(p, q)) | 111 | .clause(trueDnf.call(q), friendView.call(p, q)) |
@@ -143,12 +117,6 @@ class DnfBuilderTest { | |||
143 | 117 | ||
144 | @Test | 118 | @Test |
145 | void eliminateFalseDnfTest() { | 119 | void eliminateFalseDnfTest() { |
146 | var p = Variable.of("p"); | ||
147 | var q = Variable.of("q"); | ||
148 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
149 | var friendView = new KeyOnlyView<>(friend); | ||
150 | var falseDnf = Dnf.builder().parameter(p).build(); | ||
151 | |||
152 | var actual = Dnf.builder() | 120 | var actual = Dnf.builder() |
153 | .parameters(p, q) | 121 | .parameters(p, q) |
154 | .clause(friendView.call(p, q)) | 122 | .clause(friendView.call(p, q)) |
@@ -161,12 +129,6 @@ class DnfBuilderTest { | |||
161 | 129 | ||
162 | @Test | 130 | @Test |
163 | void alwaysTrueDnfTest() { | 131 | void alwaysTrueDnfTest() { |
164 | var p = Variable.of("p"); | ||
165 | var q = Variable.of("q"); | ||
166 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
167 | var friendView = new KeyOnlyView<>(friend); | ||
168 | var trueDnf = Dnf.builder().parameter(p).clause().build(); | ||
169 | |||
170 | var actual = Dnf.builder() | 132 | var actual = Dnf.builder() |
171 | .parameters(p, q) | 133 | .parameters(p, q) |
172 | .clause(friendView.call(p, q)) | 134 | .clause(friendView.call(p, q)) |
@@ -179,12 +141,6 @@ class DnfBuilderTest { | |||
179 | 141 | ||
180 | @Test | 142 | @Test |
181 | void alwaysFalseDnfTest() { | 143 | void alwaysFalseDnfTest() { |
182 | var p = Variable.of("p"); | ||
183 | var q = Variable.of("q"); | ||
184 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
185 | var friendView = new KeyOnlyView<>(friend); | ||
186 | var falseDnf = Dnf.builder().parameter(p).build(); | ||
187 | |||
188 | var actual = Dnf.builder() | 144 | var actual = Dnf.builder() |
189 | .parameters(p, q) | 145 | .parameters(p, q) |
190 | .clause(friendView.call(p, q), falseDnf.call(q)) | 146 | .clause(friendView.call(p, q), falseDnf.call(q)) |
@@ -196,12 +152,6 @@ class DnfBuilderTest { | |||
196 | 152 | ||
197 | @Test | 153 | @Test |
198 | void eliminateNotFalseDnfTest() { | 154 | void eliminateNotFalseDnfTest() { |
199 | var p = Variable.of("p"); | ||
200 | var q = Variable.of("q"); | ||
201 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
202 | var friendView = new KeyOnlyView<>(friend); | ||
203 | var falseDnf = Dnf.builder().parameter(p).build(); | ||
204 | |||
205 | var actual = Dnf.builder() | 155 | var actual = Dnf.builder() |
206 | .parameters(p, q) | 156 | .parameters(p, q) |
207 | .clause(not(falseDnf.call(q)), friendView.call(p, q)) | 157 | .clause(not(falseDnf.call(q)), friendView.call(p, q)) |
@@ -213,12 +163,6 @@ class DnfBuilderTest { | |||
213 | 163 | ||
214 | @Test | 164 | @Test |
215 | void eliminateNotTrueDnfTest() { | 165 | void eliminateNotTrueDnfTest() { |
216 | var p = Variable.of("p"); | ||
217 | var q = Variable.of("q"); | ||
218 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
219 | var friendView = new KeyOnlyView<>(friend); | ||
220 | var trueDnf = Dnf.builder().parameter(p).clause().build(); | ||
221 | |||
222 | var actual = Dnf.builder() | 166 | var actual = Dnf.builder() |
223 | .parameters(p, q) | 167 | .parameters(p, q) |
224 | .clause(friendView.call(p, q)) | 168 | .clause(friendView.call(p, q)) |
@@ -231,12 +175,6 @@ class DnfBuilderTest { | |||
231 | 175 | ||
232 | @Test | 176 | @Test |
233 | void alwaysNotFalseDnfTest() { | 177 | void alwaysNotFalseDnfTest() { |
234 | var p = Variable.of("p"); | ||
235 | var q = Variable.of("q"); | ||
236 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
237 | var friendView = new KeyOnlyView<>(friend); | ||
238 | var falseDnf = Dnf.builder().parameter(p).build(); | ||
239 | |||
240 | var actual = Dnf.builder() | 178 | var actual = Dnf.builder() |
241 | .parameters(p, q) | 179 | .parameters(p, q) |
242 | .clause(friendView.call(p, q)) | 180 | .clause(friendView.call(p, q)) |
@@ -249,12 +187,6 @@ class DnfBuilderTest { | |||
249 | 187 | ||
250 | @Test | 188 | @Test |
251 | void alwaysNotTrueDnfTest() { | 189 | void alwaysNotTrueDnfTest() { |
252 | var p = Variable.of("p"); | ||
253 | var q = Variable.of("q"); | ||
254 | var friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
255 | var friendView = new KeyOnlyView<>(friend); | ||
256 | var trueDnf = Dnf.builder().parameter(p).clause().build(); | ||
257 | |||
258 | var actual = Dnf.builder() | 190 | var actual = Dnf.builder() |
259 | .parameters(p, q) | 191 | .parameters(p, q) |
260 | .clause(friendView.call(p, q), not(trueDnf.call(q))) | 192 | .clause(friendView.call(p, q), not(trueDnf.call(q))) |
@@ -263,4 +195,15 @@ class DnfBuilderTest { | |||
263 | 195 | ||
264 | assertThat(actual, structurallyEqualTo(expected)); | 196 | assertThat(actual, structurallyEqualTo(expected)); |
265 | } | 197 | } |
198 | |||
199 | @Test | ||
200 | void removeDuplicateTest() { | ||
201 | var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of( | ||
202 | friendView.call(p, q), | ||
203 | friendView.call(p, q) | ||
204 | ))); | ||
205 | var expected = Dnf.of(builder -> builder.clause((p, q) -> List.of(friendView.call(p, q)))); | ||
206 | |||
207 | assertThat(actual, structurallyEqualTo(expected)); | ||
208 | } | ||
266 | } | 209 | } |
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderVariableUnificationTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderVariableUnificationTest.java new file mode 100644 index 00000000..a54ad4d6 --- /dev/null +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderVariableUnificationTest.java | |||
@@ -0,0 +1,273 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.query.dnf; | ||
7 | |||
8 | import org.junit.jupiter.api.Test; | ||
9 | import tools.refinery.store.query.view.KeyOnlyView; | ||
10 | import tools.refinery.store.query.view.SymbolView; | ||
11 | import tools.refinery.store.representation.Symbol; | ||
12 | |||
13 | import java.util.List; | ||
14 | |||
15 | import static org.hamcrest.MatcherAssert.assertThat; | ||
16 | import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo; | ||
17 | |||
18 | class DnfBuilderVariableUnificationTest { | ||
19 | private final Symbol<Boolean> friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
20 | private final Symbol<Boolean> children = new Symbol<>("friend", 2, Boolean.class, false); | ||
21 | private final SymbolView<Boolean> friendView = new KeyOnlyView<>(friend); | ||
22 | private final SymbolView<Boolean> childrenView = new KeyOnlyView<>(children); | ||
23 | |||
24 | @Test | ||
25 | void equalToParameterTest() { | ||
26 | var actual = Dnf.of(builder -> { | ||
27 | var p = builder.parameter("p"); | ||
28 | builder.clause(q -> List.of( | ||
29 | friendView.call(p, q), | ||
30 | p.isEquivalent(q) | ||
31 | )); | ||
32 | }); | ||
33 | var expected = Dnf.of(builder -> { | ||
34 | var p = builder.parameter("p"); | ||
35 | builder.clause(friendView.call(p, p)); | ||
36 | }); | ||
37 | |||
38 | assertThat(actual, structurallyEqualTo(expected)); | ||
39 | } | ||
40 | |||
41 | @Test | ||
42 | void equalToParameterReverseTest() { | ||
43 | var actual = Dnf.of(builder -> { | ||
44 | var p = builder.parameter("p"); | ||
45 | builder.clause(q -> List.of( | ||
46 | friendView.call(p, q), | ||
47 | q.isEquivalent(p) | ||
48 | )); | ||
49 | }); | ||
50 | var expected = Dnf.of(builder -> { | ||
51 | var p = builder.parameter("p"); | ||
52 | builder.clause(friendView.call(p, p)); | ||
53 | }); | ||
54 | |||
55 | assertThat(actual, structurallyEqualTo(expected)); | ||
56 | } | ||
57 | |||
58 | @Test | ||
59 | void equalQuantifiedTest() { | ||
60 | var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of( | ||
61 | friendView.call(p, q), | ||
62 | p.isEquivalent(q) | ||
63 | ))); | ||
64 | var expected = Dnf.of(builder -> builder.clause(p -> List.of(friendView.call(p, p)))); | ||
65 | |||
66 | assertThat(actual, structurallyEqualTo(expected)); | ||
67 | } | ||
68 | |||
69 | @Test | ||
70 | void equalQuantifiedTransitiveTest() { | ||
71 | var actual = Dnf.of(builder -> builder.clause((p, q, r) -> List.of( | ||
72 | friendView.call(p, q), | ||
73 | p.isEquivalent(q), | ||
74 | childrenView.call(p, r), | ||
75 | q.isEquivalent(r) | ||
76 | ))); | ||
77 | var expected = Dnf.of(builder -> builder.clause(p -> List.of( | ||
78 | friendView.call(p, p), | ||
79 | childrenView.call(p, p) | ||
80 | ))); | ||
81 | |||
82 | assertThat(actual, structurallyEqualTo(expected)); | ||
83 | } | ||
84 | |||
85 | @Test | ||
86 | void equalQuantifiedTransitiveRemoveDuplicateTest() { | ||
87 | var actual = Dnf.of(builder -> builder.clause((p, q, r) -> List.of( | ||
88 | friendView.call(p, q), | ||
89 | p.isEquivalent(q), | ||
90 | friendView.call(p, r), | ||
91 | q.isEquivalent(r) | ||
92 | ))); | ||
93 | var expected = Dnf.of(builder -> builder.clause(p -> List.of(friendView.call(p, p)))); | ||
94 | |||
95 | assertThat(actual, structurallyEqualTo(expected)); | ||
96 | } | ||
97 | |||
98 | @Test | ||
99 | void parametersEqualTest() { | ||
100 | var actual = Dnf.of(builder -> { | ||
101 | var p = builder.parameter("p"); | ||
102 | var q = builder.parameter("q"); | ||
103 | builder.clause( | ||
104 | friendView.call(p, q), | ||
105 | p.isEquivalent(q) | ||
106 | ); | ||
107 | }); | ||
108 | var expected = Dnf.of(builder -> { | ||
109 | var p = builder.parameter("p"); | ||
110 | var q = builder.parameter("q"); | ||
111 | builder.clause( | ||
112 | q.isEquivalent(p), | ||
113 | friendView.call(p, p) | ||
114 | ); | ||
115 | }); | ||
116 | |||
117 | assertThat(actual, structurallyEqualTo(expected)); | ||
118 | } | ||
119 | |||
120 | @Test | ||
121 | void parametersEqualTransitiveTest() { | ||
122 | var actual = Dnf.of(builder -> { | ||
123 | var p = builder.parameter("p"); | ||
124 | var q = builder.parameter("q"); | ||
125 | var r = builder.parameter("r"); | ||
126 | builder.clause( | ||
127 | friendView.call(p, q), | ||
128 | childrenView.call(p, r), | ||
129 | p.isEquivalent(q), | ||
130 | r.isEquivalent(q) | ||
131 | ); | ||
132 | }); | ||
133 | var expected = Dnf.of(builder -> { | ||
134 | var p = builder.parameter("p"); | ||
135 | var q = builder.parameter("q"); | ||
136 | var r = builder.parameter("r"); | ||
137 | builder.clause( | ||
138 | q.isEquivalent(p), | ||
139 | r.isEquivalent(p), | ||
140 | friendView.call(p, p), | ||
141 | childrenView.call(p, p) | ||
142 | ); | ||
143 | }); | ||
144 | |||
145 | assertThat(actual, structurallyEqualTo(expected)); | ||
146 | } | ||
147 | |||
148 | @Test | ||
149 | void parameterAndQuantifiedEqualsTest() { | ||
150 | var actual = Dnf.of(builder -> { | ||
151 | var p = builder.parameter("p"); | ||
152 | var q = builder.parameter("q"); | ||
153 | builder.clause((r) -> List.of( | ||
154 | friendView.call(p, r), | ||
155 | p.isEquivalent(r), | ||
156 | childrenView.call(q, r), | ||
157 | q.isEquivalent(r) | ||
158 | )); | ||
159 | }); | ||
160 | var expected = Dnf.of(builder -> { | ||
161 | var p = builder.parameter("p"); | ||
162 | var q = builder.parameter("q"); | ||
163 | builder.clause( | ||
164 | q.isEquivalent(p), | ||
165 | friendView.call(p, p), | ||
166 | childrenView.call(p, p) | ||
167 | ); | ||
168 | }); | ||
169 | |||
170 | assertThat(actual, structurallyEqualTo(expected)); | ||
171 | } | ||
172 | |||
173 | @Test | ||
174 | void parameterAndQuantifiedEqualsReverseFirstTest() { | ||
175 | var actual = Dnf.of(builder -> { | ||
176 | var p = builder.parameter("p"); | ||
177 | var q = builder.parameter("q"); | ||
178 | builder.clause((r) -> List.of( | ||
179 | friendView.call(p, r), | ||
180 | r.isEquivalent(p), | ||
181 | childrenView.call(q, r), | ||
182 | q.isEquivalent(r) | ||
183 | )); | ||
184 | }); | ||
185 | var expected = Dnf.of(builder -> { | ||
186 | var p = builder.parameter("p"); | ||
187 | var q = builder.parameter("q"); | ||
188 | builder.clause( | ||
189 | q.isEquivalent(p), | ||
190 | friendView.call(p, p), | ||
191 | childrenView.call(p, p) | ||
192 | ); | ||
193 | }); | ||
194 | |||
195 | assertThat(actual, structurallyEqualTo(expected)); | ||
196 | } | ||
197 | |||
198 | @Test | ||
199 | void parameterAndQuantifiedEqualsReverseSecondTest() { | ||
200 | var actual = Dnf.of(builder -> { | ||
201 | var p = builder.parameter("p"); | ||
202 | var q = builder.parameter("q"); | ||
203 | builder.clause((r) -> List.of( | ||
204 | friendView.call(p, r), | ||
205 | p.isEquivalent(r), | ||
206 | childrenView.call(q, r), | ||
207 | r.isEquivalent(q) | ||
208 | )); | ||
209 | }); | ||
210 | var expected = Dnf.of(builder -> { | ||
211 | var p = builder.parameter("p"); | ||
212 | var q = builder.parameter("q"); | ||
213 | builder.clause( | ||
214 | q.isEquivalent(p), | ||
215 | friendView.call(p, p), | ||
216 | childrenView.call(p, p) | ||
217 | ); | ||
218 | }); | ||
219 | |||
220 | assertThat(actual, structurallyEqualTo(expected)); | ||
221 | } | ||
222 | |||
223 | @Test | ||
224 | void parameterAndQuantifiedEqualsReverseBoth() { | ||
225 | var actual = Dnf.of(builder -> { | ||
226 | var p = builder.parameter("p"); | ||
227 | var q = builder.parameter("q"); | ||
228 | builder.clause((r) -> List.of( | ||
229 | friendView.call(p, r), | ||
230 | p.isEquivalent(r), | ||
231 | childrenView.call(q, r), | ||
232 | r.isEquivalent(q) | ||
233 | )); | ||
234 | }); | ||
235 | var expected = Dnf.of(builder -> { | ||
236 | var p = builder.parameter("p"); | ||
237 | var q = builder.parameter("q"); | ||
238 | builder.clause( | ||
239 | q.isEquivalent(p), | ||
240 | friendView.call(p, p), | ||
241 | childrenView.call(p, p) | ||
242 | ); | ||
243 | }); | ||
244 | |||
245 | assertThat(actual, structurallyEqualTo(expected)); | ||
246 | } | ||
247 | |||
248 | @Test | ||
249 | void parameterAndTwoQuantifiedEqualsTest() { | ||
250 | var actual = Dnf.of(builder -> { | ||
251 | var p = builder.parameter("p"); | ||
252 | var q = builder.parameter("q"); | ||
253 | builder.clause((r, s) -> List.of( | ||
254 | r.isEquivalent(s), | ||
255 | friendView.call(p, r), | ||
256 | p.isEquivalent(r), | ||
257 | childrenView.call(q, s), | ||
258 | q.isEquivalent(s) | ||
259 | )); | ||
260 | }); | ||
261 | var expected = Dnf.of(builder -> { | ||
262 | var p = builder.parameter("p"); | ||
263 | var q = builder.parameter("q"); | ||
264 | builder.clause( | ||
265 | q.isEquivalent(p), | ||
266 | friendView.call(p, p), | ||
267 | childrenView.call(p, p) | ||
268 | ); | ||
269 | }); | ||
270 | |||
271 | assertThat(actual, structurallyEqualTo(expected)); | ||
272 | } | ||
273 | } | ||
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToDefinitionStringTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java index e89ab682..2e93d78a 100644 --- a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToDefinitionStringTest.java +++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java | |||
@@ -3,10 +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; | 6 | package tools.refinery.store.query.dnf; |
7 | 7 | ||
8 | import org.junit.jupiter.api.Test; | 8 | import org.junit.jupiter.api.Test; |
9 | import tools.refinery.store.query.dnf.Dnf; | ||
10 | import tools.refinery.store.query.term.Variable; | 9 | import tools.refinery.store.query.term.Variable; |
11 | import tools.refinery.store.query.view.KeyOnlyView; | 10 | import tools.refinery.store.query.view.KeyOnlyView; |
12 | import tools.refinery.store.representation.Symbol; | 11 | import tools.refinery.store.representation.Symbol; |
@@ -43,7 +42,7 @@ class DnfToDefinitionStringTest { | |||
43 | var dnf = Dnf.builder("Example").parameter(p).clause().build(); | 42 | var dnf = Dnf.builder("Example").parameter(p).clause().build(); |
44 | 43 | ||
45 | assertThat(dnf.toDefinitionString(), is(""" | 44 | assertThat(dnf.toDefinitionString(), is(""" |
46 | pred Example(p) <-> | 45 | pred Example(@In p) <-> |
47 | <empty>. | 46 | <empty>. |
48 | """)); | 47 | """)); |
49 | } | 48 | } |
diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java index 526832c4..a5b7f85a 100644 --- a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java +++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java | |||
@@ -35,11 +35,11 @@ class MismatchDescribingDnfEqualityChecker extends DeepDnfEqualityChecker { | |||
35 | var inProgress = getInProgress(); | 35 | var inProgress = getInProgress(); |
36 | int size = inProgress.size(); | 36 | int size = inProgress.size(); |
37 | if (size <= 1) { | 37 | if (size <= 1) { |
38 | description.appendText("was ").appendText(pair.left().toDefinitionString()); | 38 | description.appendText("was ").appendText(pair.right().toDefinitionString()); |
39 | return; | 39 | return; |
40 | } | 40 | } |
41 | var last = inProgress.get(size - 1); | 41 | var last = inProgress.get(size - 1); |
42 | description.appendText("expected ").appendText(last.right().toDefinitionString()); | 42 | description.appendText("expected ").appendText(last.left().toDefinitionString()); |
43 | for (int i = size - 2; i >= 0; i--) { | 43 | for (int i = size - 2; i >= 0; i--) { |
44 | description.appendText(" called from ").appendText(inProgress.get(i).left().toString()); | 44 | description.appendText(" called from ").appendText(inProgress.get(i).left().toString()); |
45 | } | 45 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java index 594005f1..ac41d170 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java | |||
@@ -12,7 +12,7 @@ import tools.refinery.store.query.dnf.DnfClause; | |||
12 | import tools.refinery.store.query.literal.CallLiteral; | 12 | import tools.refinery.store.query.literal.CallLiteral; |
13 | import tools.refinery.store.query.literal.CallPolarity; | 13 | import tools.refinery.store.query.literal.CallPolarity; |
14 | import tools.refinery.store.query.literal.Literal; | 14 | import tools.refinery.store.query.literal.Literal; |
15 | import tools.refinery.store.query.term.DataVariable; | 15 | import tools.refinery.store.query.term.NodeVariable; |
16 | import tools.refinery.store.query.term.Variable; | 16 | import tools.refinery.store.query.term.Variable; |
17 | import tools.refinery.store.reasoning.ReasoningAdapter; | 17 | import tools.refinery.store.reasoning.ReasoningAdapter; |
18 | import tools.refinery.store.reasoning.literal.ModalConstraint; | 18 | import tools.refinery.store.reasoning.literal.ModalConstraint; |
@@ -21,7 +21,7 @@ import tools.refinery.store.reasoning.literal.PartialLiterals; | |||
21 | import tools.refinery.store.util.CycleDetectingMapper; | 21 | import tools.refinery.store.util.CycleDetectingMapper; |
22 | 22 | ||
23 | import java.util.ArrayList; | 23 | import java.util.ArrayList; |
24 | import java.util.HashSet; | 24 | import java.util.LinkedHashSet; |
25 | import java.util.List; | 25 | import java.util.List; |
26 | 26 | ||
27 | public class DnfLifter { | 27 | public class DnfLifter { |
@@ -36,10 +36,10 @@ public class DnfLifter { | |||
36 | var modality = modalDnf.modality(); | 36 | var modality = modalDnf.modality(); |
37 | var dnf = modalDnf.dnf(); | 37 | var dnf = modalDnf.dnf(); |
38 | var builder = Dnf.builder(); | 38 | var builder = Dnf.builder(); |
39 | builder.parameters(dnf.getParameters()); | 39 | builder.symbolicParameters(dnf.getSymbolicParameters()); |
40 | boolean changed = false; | 40 | boolean changed = false; |
41 | for (var clause : dnf.getClauses()) { | 41 | for (var clause : dnf.getClauses()) { |
42 | if (liftClause(modality, clause, builder)) { | 42 | if (liftClause(modality, dnf, clause, builder)) { |
43 | changed = true; | 43 | changed = true; |
44 | } | 44 | } |
45 | } | 45 | } |
@@ -49,12 +49,9 @@ public class DnfLifter { | |||
49 | return dnf; | 49 | return dnf; |
50 | } | 50 | } |
51 | 51 | ||
52 | private boolean liftClause(Modality modality, DnfClause clause, DnfBuilder builder) { | 52 | private boolean liftClause(Modality modality, Dnf originalDnf, DnfClause clause, DnfBuilder builder) { |
53 | boolean changed = false; | 53 | boolean changed = false; |
54 | var quantifiedVariables = new HashSet<>(clause.boundVariables() | 54 | var quantifiedVariables = getQuantifiedDataVariables(originalDnf, clause); |
55 | .stream() | ||
56 | .filter(DataVariable.class::isInstance) | ||
57 | .toList()); | ||
58 | var literals = clause.literals(); | 55 | var literals = clause.literals(); |
59 | var liftedLiterals = new ArrayList<Literal>(literals.size()); | 56 | var liftedLiterals = new ArrayList<Literal>(literals.size()); |
60 | for (var literal : literals) { | 57 | for (var literal : literals) { |
@@ -81,6 +78,16 @@ public class DnfLifter { | |||
81 | return changed || !quantifiedVariables.isEmpty(); | 78 | return changed || !quantifiedVariables.isEmpty(); |
82 | } | 79 | } |
83 | 80 | ||
81 | private static LinkedHashSet<Variable> getQuantifiedDataVariables(Dnf originalDnf, DnfClause clause) { | ||
82 | var quantifiedVariables = new LinkedHashSet<>(clause.positiveVariables()); | ||
83 | for (var symbolicParameter : originalDnf.getSymbolicParameters()) { | ||
84 | // The existence of parameters will be checked outside this DNF. | ||
85 | quantifiedVariables.remove(symbolicParameter.getVariable()); | ||
86 | } | ||
87 | quantifiedVariables.removeIf(variable -> !(variable instanceof NodeVariable)); | ||
88 | return quantifiedVariables; | ||
89 | } | ||
90 | |||
84 | @Nullable | 91 | @Nullable |
85 | private Variable isExistsLiteralForVariable(Modality modality, Literal literal) { | 92 | private Variable isExistsLiteralForVariable(Modality modality, Literal literal) { |
86 | if (literal instanceof CallLiteral callLiteral && | 93 | if (literal instanceof CallLiteral callLiteral && |
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 7fa98104..ce557d82 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 | |||
@@ -8,7 +8,7 @@ package tools.refinery.store.reasoning.literal; | |||
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.literal.LiteralReduction; |
11 | import tools.refinery.store.query.term.Sort; | 11 | import tools.refinery.store.query.term.Parameter; |
12 | 12 | ||
13 | import java.util.List; | 13 | import java.util.List; |
14 | 14 | ||
@@ -21,8 +21,8 @@ public record ModalConstraint(Modality modality, Constraint constraint) implemen | |||
21 | } | 21 | } |
22 | 22 | ||
23 | @Override | 23 | @Override |
24 | public List<Sort> getSorts() { | 24 | public List<Parameter> getParameters() { |
25 | return constraint.getSorts(); | 25 | return constraint.getParameters(); |
26 | } | 26 | } |
27 | 27 | ||
28 | @Override | 28 | @Override |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java index fc3dc074..1f74ce38 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java | |||
@@ -6,8 +6,7 @@ | |||
6 | package tools.refinery.store.reasoning.representation; | 6 | package tools.refinery.store.reasoning.representation; |
7 | 7 | ||
8 | import tools.refinery.store.query.Constraint; | 8 | import tools.refinery.store.query.Constraint; |
9 | import tools.refinery.store.query.term.NodeSort; | 9 | import tools.refinery.store.query.term.Parameter; |
10 | import tools.refinery.store.query.term.Sort; | ||
11 | import tools.refinery.store.representation.AbstractDomain; | 10 | import tools.refinery.store.representation.AbstractDomain; |
12 | import tools.refinery.store.representation.TruthValue; | 11 | import tools.refinery.store.representation.TruthValue; |
13 | import tools.refinery.store.representation.TruthValueDomain; | 12 | import tools.refinery.store.representation.TruthValueDomain; |
@@ -32,10 +31,10 @@ public record PartialRelation(String name, int arity) implements PartialSymbol<T | |||
32 | } | 31 | } |
33 | 32 | ||
34 | @Override | 33 | @Override |
35 | public List<Sort> getSorts() { | 34 | public List<Parameter> getParameters() { |
36 | var sorts = new Sort[arity()]; | 35 | var parameters = new Parameter[arity]; |
37 | Arrays.fill(sorts, NodeSort.INSTANCE); | 36 | Arrays.fill(parameters, Parameter.NODE_IN_OUT); |
38 | return List.of(sorts); | 37 | return List.of(parameters); |
39 | } | 38 | } |
40 | 39 | ||
41 | @Override | 40 | @Override |