diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-08-18 20:35:21 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-08-18 20:35:21 +0200 |
commit | ecf62ce9828a1fdf45e81d9bf91655513a0e26d6 (patch) | |
tree | b1e0e2f00f81fc795d5654df7942c9be2fd5c11b | |
parent | build: fix deprecation warning (diff) | |
download | refinery-ecf62ce9828a1fdf45e81d9bf91655513a0e26d6.tar.gz refinery-ecf62ce9828a1fdf45e81d9bf91655513a0e26d6.tar.zst refinery-ecf62ce9828a1fdf45e81d9bf91655513a0e26d6.zip |
feat: predicate semantics
3 files changed, 281 insertions, 29 deletions
diff --git a/subprojects/frontend/src/index.tsx b/subprojects/frontend/src/index.tsx index 077bae79..8cbb8fbc 100644 --- a/subprojects/frontend/src/index.tsx +++ b/subprojects/frontend/src/index.tsx | |||
@@ -17,7 +17,7 @@ class Person { | |||
17 | } | 17 | } |
18 | 18 | ||
19 | class Post { | 19 | class Post { |
20 | container Person[1] author opposite posts | 20 | container Person author opposite posts |
21 | Post replyTo | 21 | Post replyTo |
22 | } | 22 | } |
23 | 23 | ||
@@ -26,6 +26,7 @@ error replyToNotFriend(Post x, Post y) <-> | |||
26 | replyTo(x, y), | 26 | replyTo(x, y), |
27 | author(x, xAuthor), | 27 | author(x, xAuthor), |
28 | author(y, yAuthor), | 28 | author(y, yAuthor), |
29 | xAuthor != yAuthor, | ||
29 | !friend(xAuthor, yAuthor). | 30 | !friend(xAuthor, yAuthor). |
30 | 31 | ||
31 | error replyToCycle(Post x) <-> replyTo+(x, x). | 32 | error replyToCycle(Post x) <-> replyTo+(x, x). |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java index d2990aff..12bb94c2 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java | |||
@@ -14,6 +14,12 @@ import tools.refinery.language.utils.BuiltinSymbols; | |||
14 | import tools.refinery.language.utils.ProblemDesugarer; | 14 | import tools.refinery.language.utils.ProblemDesugarer; |
15 | import tools.refinery.language.utils.ProblemUtil; | 15 | import tools.refinery.language.utils.ProblemUtil; |
16 | import tools.refinery.store.model.ModelStoreBuilder; | 16 | import tools.refinery.store.model.ModelStoreBuilder; |
17 | import tools.refinery.store.query.Constraint; | ||
18 | import tools.refinery.store.query.dnf.Query; | ||
19 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
20 | import tools.refinery.store.query.literal.*; | ||
21 | import tools.refinery.store.query.term.NodeVariable; | ||
22 | import tools.refinery.store.query.term.Variable; | ||
17 | import tools.refinery.store.reasoning.ReasoningAdapter; | 23 | import tools.refinery.store.reasoning.ReasoningAdapter; |
18 | import tools.refinery.store.reasoning.representation.PartialRelation; | 24 | import tools.refinery.store.reasoning.representation.PartialRelation; |
19 | import tools.refinery.store.reasoning.seed.ModelSeed; | 25 | import tools.refinery.store.reasoning.seed.ModelSeed; |
@@ -26,15 +32,14 @@ import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslat | |||
26 | import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; | 32 | import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; |
27 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | 33 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; |
28 | import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMultiplicity; | 34 | import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMultiplicity; |
35 | import tools.refinery.store.reasoning.translator.predicate.PredicateTranslator; | ||
29 | import tools.refinery.store.representation.TruthValue; | 36 | import tools.refinery.store.representation.TruthValue; |
30 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | 37 | import tools.refinery.store.representation.cardinality.CardinalityInterval; |
31 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | 38 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; |
32 | import tools.refinery.store.representation.cardinality.UpperCardinalities; | 39 | import tools.refinery.store.representation.cardinality.UpperCardinalities; |
33 | import tools.refinery.store.tuple.Tuple; | 40 | import tools.refinery.store.tuple.Tuple; |
34 | 41 | ||
35 | import java.util.ArrayList; | 42 | import java.util.*; |
36 | import java.util.LinkedHashMap; | ||
37 | import java.util.Map; | ||
38 | 43 | ||
39 | public class ModelInitializer { | 44 | public class ModelInitializer { |
40 | @Inject | 45 | @Inject |
@@ -45,6 +50,8 @@ public class ModelInitializer { | |||
45 | 50 | ||
46 | private Problem problem; | 51 | private Problem problem; |
47 | 52 | ||
53 | private ModelStoreBuilder storeBuilder; | ||
54 | |||
48 | private BuiltinSymbols builtinSymbols; | 55 | private BuiltinSymbols builtinSymbols; |
49 | 56 | ||
50 | private PartialRelation nodeRelation; | 57 | private PartialRelation nodeRelation; |
@@ -61,6 +68,8 @@ public class ModelInitializer { | |||
61 | 68 | ||
62 | private Metamodel metamodel; | 69 | private Metamodel metamodel; |
63 | 70 | ||
71 | private ModelSeed modelSeed; | ||
72 | |||
64 | public int getNodeCount() { | 73 | public int getNodeCount() { |
65 | return nodeTrace.size(); | 74 | return nodeTrace.size(); |
66 | } | 75 | } |
@@ -73,24 +82,24 @@ public class ModelInitializer { | |||
73 | return relationTrace; | 82 | return relationTrace; |
74 | } | 83 | } |
75 | 84 | ||
76 | public ModelSeed createModel(Problem problem, ModelStoreBuilder builder) { | 85 | public ModelSeed createModel(Problem problem, ModelStoreBuilder storeBuilder) { |
77 | this.problem = problem; | 86 | this.problem = problem; |
87 | this.storeBuilder = storeBuilder; | ||
78 | builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException( | 88 | builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException( |
79 | "Problem has no builtin library")); | 89 | "Problem has no builtin library")); |
80 | var nodeInfo = collectPartialRelation(builtinSymbols.node(), 1, TruthValue.TRUE, TruthValue.TRUE); | 90 | var nodeInfo = collectPartialRelation(builtinSymbols.node(), 1, TruthValue.TRUE, TruthValue.TRUE); |
81 | nodeRelation = nodeInfo.partialRelation(); | 91 | nodeRelation = nodeInfo.partialRelation(); |
82 | metamodelBuilder.type(nodeRelation); | 92 | metamodelBuilder.type(nodeRelation); |
83 | relationInfoMap.put(builtinSymbols.exists(), new RelationInfo(ReasoningAdapter.EXISTS_SYMBOL, null, | 93 | putRelationInfo(builtinSymbols.exists(), new RelationInfo(ReasoningAdapter.EXISTS_SYMBOL, null, |
84 | TruthValue.TRUE)); | 94 | TruthValue.TRUE)); |
85 | relationInfoMap.put(builtinSymbols.equals(), new RelationInfo(ReasoningAdapter.EQUALS_SYMBOL, | 95 | putRelationInfo(builtinSymbols.equals(), new RelationInfo(ReasoningAdapter.EQUALS_SYMBOL, |
86 | (TruthValue) null, | 96 | (TruthValue) null, |
87 | null)); | 97 | null)); |
88 | relationInfoMap.put(builtinSymbols.contained(), | 98 | putRelationInfo(builtinSymbols.contained(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINED_SYMBOL, |
89 | new RelationInfo(ContainmentHierarchyTranslator.CONTAINED_SYMBOL, | 99 | null, TruthValue.UNKNOWN)); |
90 | null, TruthValue.UNKNOWN)); | 100 | putRelationInfo(builtinSymbols.contains(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINS_SYMBOL, |
91 | relationInfoMap.put(builtinSymbols.contains(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINS_SYMBOL, | ||
92 | null, TruthValue.UNKNOWN)); | 101 | null, TruthValue.UNKNOWN)); |
93 | relationInfoMap.put(builtinSymbols.invalidNumberOfContainers(), | 102 | putRelationInfo(builtinSymbols.invalidNumberOfContainers(), |
94 | new RelationInfo(ContainmentHierarchyTranslator.INVALID_NUMBER_OF_CONTAINERS, TruthValue.FALSE, | 103 | new RelationInfo(ContainmentHierarchyTranslator.INVALID_NUMBER_OF_CONTAINERS, TruthValue.FALSE, |
95 | TruthValue.FALSE)); | 104 | TruthValue.FALSE)); |
96 | collectNodes(); | 105 | collectNodes(); |
@@ -98,8 +107,8 @@ public class ModelInitializer { | |||
98 | collectMetamodel(); | 107 | collectMetamodel(); |
99 | metamodel = metamodelBuilder.build(); | 108 | metamodel = metamodelBuilder.build(); |
100 | collectAssertions(); | 109 | collectAssertions(); |
101 | builder.with(new MultiObjectTranslator()); | 110 | storeBuilder.with(new MultiObjectTranslator()); |
102 | builder.with(new MetamodelTranslator(metamodel)); | 111 | storeBuilder.with(new MetamodelTranslator(metamodel)); |
103 | relationTrace = new LinkedHashMap<>(relationInfoMap.size()); | 112 | relationTrace = new LinkedHashMap<>(relationInfoMap.size()); |
104 | int nodeCount = getNodeCount(); | 113 | int nodeCount = getNodeCount(); |
105 | var modelSeedBuilder = ModelSeed.builder(nodeCount); | 114 | var modelSeedBuilder = ModelSeed.builder(nodeCount); |
@@ -110,7 +119,9 @@ public class ModelInitializer { | |||
110 | relationTrace.put(relation, partialRelation); | 119 | relationTrace.put(relation, partialRelation); |
111 | modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount)); | 120 | modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount)); |
112 | } | 121 | } |
113 | return modelSeedBuilder.build(); | 122 | modelSeed = modelSeedBuilder.build(); |
123 | collectPredicates(); | ||
124 | return modelSeed; | ||
114 | } | 125 | } |
115 | 126 | ||
116 | private void collectNodes() { | 127 | private void collectNodes() { |
@@ -142,16 +153,16 @@ public class ModelInitializer { | |||
142 | private void collectPartialSymbols() { | 153 | private void collectPartialSymbols() { |
143 | for (var statement : problem.getStatements()) { | 154 | for (var statement : problem.getStatements()) { |
144 | if (statement instanceof ClassDeclaration classDeclaration) { | 155 | if (statement instanceof ClassDeclaration classDeclaration) { |
145 | collectClassDeclaration(classDeclaration); | 156 | collectClassDeclarationSymbols(classDeclaration); |
146 | } else if (statement instanceof EnumDeclaration enumDeclaration) { | 157 | } else if (statement instanceof EnumDeclaration enumDeclaration) { |
147 | collectPartialRelation(enumDeclaration, 1, null, TruthValue.FALSE); | 158 | collectPartialRelation(enumDeclaration, 1, null, TruthValue.FALSE); |
148 | } else if (statement instanceof PredicateDefinition predicateDefinition) { | 159 | } else if (statement instanceof PredicateDefinition predicateDefinition) { |
149 | // TODO Implement predicate definitions | 160 | collectPredicateDefinitionSymbol(predicateDefinition); |
150 | } | 161 | } |
151 | } | 162 | } |
152 | } | 163 | } |
153 | 164 | ||
154 | private void collectClassDeclaration(ClassDeclaration classDeclaration) { | 165 | private void collectClassDeclarationSymbols(ClassDeclaration classDeclaration) { |
155 | collectPartialRelation(classDeclaration, 1, null, TruthValue.UNKNOWN); | 166 | collectPartialRelation(classDeclaration, 1, null, TruthValue.UNKNOWN); |
156 | for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) { | 167 | for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) { |
157 | if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) { | 168 | if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) { |
@@ -166,6 +177,15 @@ public class ModelInitializer { | |||
166 | } | 177 | } |
167 | } | 178 | } |
168 | 179 | ||
180 | private void collectPredicateDefinitionSymbol(PredicateDefinition predicateDefinition) { | ||
181 | int arity = predicateDefinition.getParameters().size(); | ||
182 | if (predicateDefinition.isError()) { | ||
183 | collectPartialRelation(predicateDefinition, arity, TruthValue.FALSE, TruthValue.FALSE); | ||
184 | } else { | ||
185 | collectPartialRelation(predicateDefinition, arity, null, TruthValue.UNKNOWN); | ||
186 | } | ||
187 | } | ||
188 | |||
169 | private void putRelationInfo(Relation relation, RelationInfo info) { | 189 | private void putRelationInfo(Relation relation, RelationInfo info) { |
170 | relationInfoMap.put(relation, info); | 190 | relationInfoMap.put(relation, info); |
171 | partialRelationInfoMap.put(info.partialRelation(), info); | 191 | partialRelationInfoMap.put(info.partialRelation(), info); |
@@ -196,8 +216,7 @@ public class ModelInitializer { | |||
196 | } | 216 | } |
197 | 217 | ||
198 | private void collectEnumMetamodel(EnumDeclaration enumDeclaration) { | 218 | private void collectEnumMetamodel(EnumDeclaration enumDeclaration) { |
199 | var info = getRelationInfo(enumDeclaration); | 219 | metamodelBuilder.type(getPartialRelation(enumDeclaration), nodeRelation); |
200 | metamodelBuilder.type(info.partialRelation(), nodeRelation); | ||
201 | } | 220 | } |
202 | 221 | ||
203 | private void collectClassDeclarationMetamodel(ClassDeclaration classDeclaration) { | 222 | private void collectClassDeclarationMetamodel(ClassDeclaration classDeclaration) { |
@@ -205,10 +224,9 @@ public class ModelInitializer { | |||
205 | var partialSuperTypes = new ArrayList<PartialRelation>(superTypes.size() + 1); | 224 | var partialSuperTypes = new ArrayList<PartialRelation>(superTypes.size() + 1); |
206 | partialSuperTypes.add(nodeRelation); | 225 | partialSuperTypes.add(nodeRelation); |
207 | for (var superType : superTypes) { | 226 | for (var superType : superTypes) { |
208 | partialSuperTypes.add(getRelationInfo(superType).partialRelation()); | 227 | partialSuperTypes.add(getPartialRelation(superType)); |
209 | } | 228 | } |
210 | var info = getRelationInfo(classDeclaration); | 229 | metamodelBuilder.type(getPartialRelation(classDeclaration), classDeclaration.isAbstract(), |
211 | metamodelBuilder.type(info.partialRelation(), classDeclaration.isAbstract(), | ||
212 | partialSuperTypes); | 230 | partialSuperTypes); |
213 | for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) { | 231 | for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) { |
214 | if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) { | 232 | if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) { |
@@ -221,14 +239,14 @@ public class ModelInitializer { | |||
221 | 239 | ||
222 | private void collectReferenceDeclarationMetamodel(ClassDeclaration classDeclaration, | 240 | private void collectReferenceDeclarationMetamodel(ClassDeclaration classDeclaration, |
223 | ReferenceDeclaration referenceDeclaration) { | 241 | ReferenceDeclaration referenceDeclaration) { |
224 | var relation = getRelationInfo(referenceDeclaration).partialRelation(); | 242 | var relation = getPartialRelation(referenceDeclaration); |
225 | var source = getRelationInfo(classDeclaration).partialRelation(); | 243 | var source = getPartialRelation(classDeclaration); |
226 | var target = getRelationInfo(referenceDeclaration.getReferenceType()).partialRelation(); | 244 | var target = getPartialRelation(referenceDeclaration.getReferenceType()); |
227 | boolean containment = referenceDeclaration.getKind() == ReferenceKind.CONTAINMENT; | 245 | boolean containment = referenceDeclaration.getKind() == ReferenceKind.CONTAINMENT; |
228 | var opposite = referenceDeclaration.getOpposite(); | 246 | var opposite = referenceDeclaration.getOpposite(); |
229 | PartialRelation oppositeRelation = null; | 247 | PartialRelation oppositeRelation = null; |
230 | if (opposite != null) { | 248 | if (opposite != null) { |
231 | oppositeRelation = getRelationInfo(opposite).partialRelation(); | 249 | oppositeRelation = getPartialRelation(opposite); |
232 | } | 250 | } |
233 | var multiplicity = getMultiplicityConstraint(referenceDeclaration); | 251 | var multiplicity = getMultiplicityConstraint(referenceDeclaration); |
234 | metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation); | 252 | metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation); |
@@ -279,10 +297,9 @@ public class ModelInitializer { | |||
279 | } | 297 | } |
280 | var newNodeId = getNodeId(newNode); | 298 | var newNodeId = getNodeId(newNode); |
281 | collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN); | 299 | collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN); |
282 | var info = getRelationInfo(classDeclaration); | ||
283 | var tuple = Tuple.of(newNodeId); | 300 | var tuple = Tuple.of(newNodeId); |
284 | mergeValue(classDeclaration, tuple, TruthValue.TRUE); | 301 | mergeValue(classDeclaration, tuple, TruthValue.TRUE); |
285 | var typeInfo = metamodel.typeHierarchy().getAnalysisResult(info.partialRelation()); | 302 | var typeInfo = metamodel.typeHierarchy().getAnalysisResult(getPartialRelation(classDeclaration)); |
286 | for (var subType : typeInfo.getDirectSubtypes()) { | 303 | for (var subType : typeInfo.getDirectSubtypes()) { |
287 | partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE); | 304 | partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE); |
288 | } | 305 | } |
@@ -336,6 +353,10 @@ public class ModelInitializer { | |||
336 | return info; | 353 | return info; |
337 | } | 354 | } |
338 | 355 | ||
356 | private PartialRelation getPartialRelation(Relation relation) { | ||
357 | return getRelationInfo(relation).partialRelation(); | ||
358 | } | ||
359 | |||
339 | private int getNodeId(Node node) { | 360 | private int getNodeId(Node node) { |
340 | return nodeTrace.getOrThrow(node); | 361 | return nodeTrace.getOrThrow(node); |
341 | } | 362 | } |
@@ -369,6 +390,151 @@ public class ModelInitializer { | |||
369 | }; | 390 | }; |
370 | } | 391 | } |
371 | 392 | ||
393 | private void collectPredicates() { | ||
394 | for (var statement : problem.getStatements()) { | ||
395 | if (statement instanceof PredicateDefinition predicateDefinition) { | ||
396 | collectPredicateDefinition(predicateDefinition); | ||
397 | } | ||
398 | } | ||
399 | } | ||
400 | |||
401 | private void collectPredicateDefinition(PredicateDefinition predicateDefinition) { | ||
402 | var partialRelation = getPartialRelation(predicateDefinition); | ||
403 | var query = toQuery(partialRelation.name(), predicateDefinition); | ||
404 | boolean mutable; | ||
405 | TruthValue defaultValue; | ||
406 | if (predicateDefinition.isError()) { | ||
407 | mutable = false; | ||
408 | defaultValue = TruthValue.FALSE; | ||
409 | } else { | ||
410 | var seed = modelSeed.getSeed(partialRelation); | ||
411 | defaultValue = seed.reducedValue() == TruthValue.FALSE ? TruthValue.FALSE : TruthValue.UNKNOWN; | ||
412 | var cursor = seed.getCursor(defaultValue, getNodeCount()); | ||
413 | // The symbol should be mutable if there is at least one non-default entry in the seed. | ||
414 | mutable = cursor.move(); | ||
415 | } | ||
416 | var translator = new PredicateTranslator(partialRelation, query, mutable, defaultValue); | ||
417 | storeBuilder.with(translator); | ||
418 | } | ||
419 | |||
420 | private RelationalQuery toQuery(String name, PredicateDefinition predicateDefinition) { | ||
421 | var problemParameters = predicateDefinition.getParameters(); | ||
422 | int arity = problemParameters.size(); | ||
423 | var parameters = new NodeVariable[arity]; | ||
424 | var parameterMap = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(arity); | ||
425 | var commonLiterals = new ArrayList<Literal>(); | ||
426 | for (int i = 0; i < arity; i++) { | ||
427 | var problemParameter = problemParameters.get(i); | ||
428 | var parameter = Variable.of(problemParameter.getName()); | ||
429 | parameters[i] = parameter; | ||
430 | parameterMap.put(problemParameter, parameter); | ||
431 | var parameterType = problemParameter.getParameterType(); | ||
432 | if (parameterType != null) { | ||
433 | var partialType = getPartialRelation(parameterType); | ||
434 | commonLiterals.add(partialType.call(parameter)); | ||
435 | } | ||
436 | } | ||
437 | var builder = Query.builder(name).parameters(parameters); | ||
438 | for (var body : predicateDefinition.getBodies()) { | ||
439 | var localScope = extendScope(parameterMap, body.getImplicitVariables()); | ||
440 | var problemLiterals = body.getLiterals(); | ||
441 | var literals = new ArrayList<Literal>(commonLiterals); | ||
442 | for (var problemLiteral : problemLiterals) { | ||
443 | toLiterals(problemLiteral, localScope, literals); | ||
444 | } | ||
445 | builder.clause(literals); | ||
446 | } | ||
447 | return builder.build(); | ||
448 | } | ||
449 | |||
450 | private Map<tools.refinery.language.model.problem.Variable, Variable> extendScope( | ||
451 | Map<tools.refinery.language.model.problem.Variable, Variable> existing, | ||
452 | Collection<? extends tools.refinery.language.model.problem.Variable> newVariables) { | ||
453 | if (newVariables.isEmpty()) { | ||
454 | return existing; | ||
455 | } | ||
456 | int localScopeSize = existing.size() + newVariables.size(); | ||
457 | var localScope = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(localScopeSize); | ||
458 | localScope.putAll(existing); | ||
459 | for (var newVariable : newVariables) { | ||
460 | localScope.put(newVariable, Variable.of(newVariable.getName())); | ||
461 | } | ||
462 | return localScope; | ||
463 | } | ||
464 | |||
465 | private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope, | ||
466 | List<Literal> literals) { | ||
467 | if (expr instanceof LogicConstant logicConstant) { | ||
468 | switch (logicConstant.getLogicValue()) { | ||
469 | case TRUE -> literals.add(BooleanLiteral.TRUE); | ||
470 | case FALSE -> literals.add(BooleanLiteral.FALSE); | ||
471 | default -> throw new IllegalArgumentException("Unsupported literal: " + expr); | ||
472 | } | ||
473 | } else if (expr instanceof Atom atom) { | ||
474 | var target = getPartialRelation(atom.getRelation()); | ||
475 | var polarity = atom.isTransitiveClosure() ? CallPolarity.TRANSITIVE : CallPolarity.POSITIVE; | ||
476 | var argumentList = toArgumentList(atom.getArguments(), localScope, literals); | ||
477 | literals.add(target.call(polarity, argumentList)); | ||
478 | } else if (expr instanceof NegationExpr negationExpr) { | ||
479 | var body = negationExpr.getBody(); | ||
480 | if (!(body instanceof Atom atom)) { | ||
481 | throw new IllegalArgumentException("Cannot negate literal: " + body); | ||
482 | } | ||
483 | var target = getPartialRelation(atom.getRelation()); | ||
484 | Constraint constraint; | ||
485 | if (atom.isTransitiveClosure()) { | ||
486 | constraint = Query.of(target.name() + "#transitive", (builder, p1, p2) -> builder.clause( | ||
487 | target.callTransitive(p1, p2) | ||
488 | )).getDnf(); | ||
489 | } else { | ||
490 | constraint = target; | ||
491 | } | ||
492 | var negatedScope = extendScope(localScope, negationExpr.getImplicitVariables()); | ||
493 | var argumentList = toArgumentList(atom.getArguments(), negatedScope, literals); | ||
494 | literals.add(constraint.call(CallPolarity.NEGATIVE, argumentList)); | ||
495 | } else if (expr instanceof ComparisonExpr comparisonExpr) { | ||
496 | var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()), | ||
497 | localScope, literals); | ||
498 | boolean positive = switch (comparisonExpr.getOp()) { | ||
499 | case EQ -> true; | ||
500 | case NOT_EQ -> false; | ||
501 | default -> throw new IllegalArgumentException("Unsupported operator: " + comparisonExpr.getOp()); | ||
502 | }; | ||
503 | literals.add(new EquivalenceLiteral(positive, argumentList.get(0), argumentList.get(1))); | ||
504 | } else { | ||
505 | throw new IllegalArgumentException("Unsupported literal: " + expr); | ||
506 | } | ||
507 | } | ||
508 | |||
509 | private List<Variable> toArgumentList( | ||
510 | List<Expr> expressions, Map<tools.refinery.language.model.problem.Variable, Variable> localScope, | ||
511 | List<Literal> literals) { | ||
512 | var argumentList = new ArrayList<Variable>(expressions.size()); | ||
513 | for (var expr : expressions) { | ||
514 | if (!(expr instanceof VariableOrNodeExpr variableOrNodeExpr)) { | ||
515 | throw new IllegalArgumentException("Unsupported argument: " + expr); | ||
516 | } | ||
517 | var variableOrNode = variableOrNodeExpr.getVariableOrNode(); | ||
518 | if (variableOrNode instanceof Node node) { | ||
519 | int nodeId = getNodeId(node); | ||
520 | var tempVariable = Variable.of(semanticsUtils.getName(node).orElse("_" + nodeId)); | ||
521 | literals.add(new ConstantLiteral(tempVariable, nodeId)); | ||
522 | argumentList.add(tempVariable); | ||
523 | } else if (variableOrNode instanceof tools.refinery.language.model.problem.Variable problemVariable) { | ||
524 | if (variableOrNodeExpr.getSingletonVariable() == problemVariable) { | ||
525 | argumentList.add(Variable.of(problemVariable.getName())); | ||
526 | } else { | ||
527 | var variable = localScope.get(problemVariable); | ||
528 | if (variable == null) { | ||
529 | throw new IllegalArgumentException("Unknown variable: " + problemVariable.getName()); | ||
530 | } | ||
531 | argumentList.add(variable); | ||
532 | } | ||
533 | } | ||
534 | } | ||
535 | return argumentList; | ||
536 | } | ||
537 | |||
372 | private record RelationInfo(PartialRelation partialRelation, DecisionTree assertions, | 538 | private record RelationInfo(PartialRelation partialRelation, DecisionTree assertions, |
373 | DecisionTree defaultAssertions) { | 539 | DecisionTree defaultAssertions) { |
374 | public RelationInfo(String name, int arity, TruthValue value, TruthValue defaultValue) { | 540 | public RelationInfo(String name, int arity, TruthValue value, TruthValue defaultValue) { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateTranslator.java new file mode 100644 index 00000000..ee022f2d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateTranslator.java | |||
@@ -0,0 +1,85 @@ | |||
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.reasoning.translator.predicate; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
10 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
12 | import tools.refinery.store.query.literal.Literal; | ||
13 | import tools.refinery.store.query.term.NodeVariable; | ||
14 | import tools.refinery.store.query.term.Variable; | ||
15 | import tools.refinery.store.query.view.ForbiddenView; | ||
16 | import tools.refinery.store.query.view.MayView; | ||
17 | import tools.refinery.store.query.view.MustView; | ||
18 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
19 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
20 | import tools.refinery.store.representation.Symbol; | ||
21 | import tools.refinery.store.representation.TruthValue; | ||
22 | |||
23 | import static tools.refinery.store.query.literal.Literals.not; | ||
24 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | ||
25 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | ||
26 | |||
27 | public class PredicateTranslator implements ModelStoreConfiguration { | ||
28 | private final PartialRelation relation; | ||
29 | private final RelationalQuery query; | ||
30 | private final boolean mutable; | ||
31 | private final TruthValue defaultValue; | ||
32 | |||
33 | public PredicateTranslator(PartialRelation relation, RelationalQuery query, boolean mutable, | ||
34 | TruthValue defaultValue) { | ||
35 | if (relation.arity() != query.arity()) { | ||
36 | throw new IllegalArgumentException("Expected arity %d query for partial relation %s, got %d instead" | ||
37 | .formatted(relation.arity(), relation, query.arity())); | ||
38 | } | ||
39 | if (defaultValue.must()) { | ||
40 | throw new IllegalArgumentException("Default value must be UNKNOWN or FALSE"); | ||
41 | } | ||
42 | this.relation = relation; | ||
43 | this.query = query; | ||
44 | this.mutable = mutable; | ||
45 | this.defaultValue = defaultValue; | ||
46 | } | ||
47 | |||
48 | @Override | ||
49 | public void apply(ModelStoreBuilder storeBuilder) { | ||
50 | var translator = PartialRelationTranslator.of(relation) | ||
51 | .query(query); | ||
52 | if (mutable) { | ||
53 | var symbol = Symbol.of(relation.name(), relation.arity(), TruthValue.class, defaultValue); | ||
54 | translator.symbol(symbol); | ||
55 | |||
56 | var parameters = new NodeVariable[relation.arity()]; | ||
57 | for (int i = 0; i < parameters.length; i++) { | ||
58 | parameters[i] = Variable.of("p" + i); | ||
59 | } | ||
60 | |||
61 | var must = Query.builder() | ||
62 | .parameters(parameters) | ||
63 | .clause(must(query.call(parameters))) | ||
64 | .clause(new MustView(symbol).call(parameters)) | ||
65 | .build(); | ||
66 | translator.must(must); | ||
67 | |||
68 | var mayLiterals = new Literal[2]; | ||
69 | mayLiterals[0] = may(query.call(parameters)); | ||
70 | if (defaultValue.may()) { | ||
71 | mayLiterals[1] = not(new ForbiddenView(symbol).call(parameters)); | ||
72 | } else { | ||
73 | mayLiterals[1] = new MayView(symbol).call(parameters); | ||
74 | } | ||
75 | var may = Query.builder() | ||
76 | .parameters(parameters) | ||
77 | .clause(mayLiterals) | ||
78 | .build(); | ||
79 | translator.may(may); | ||
80 | } else if (!defaultValue.may()) { | ||
81 | translator.mayNever(); | ||
82 | } | ||
83 | storeBuilder.with(translator); | ||
84 | } | ||
85 | } | ||