diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-12-06 23:52:07 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-12-08 21:48:48 +0100 |
commit | d40ec70132ebb324873cb8c3868eb65309f46f8c (patch) | |
tree | 31c9ca6e5454f61868b4123574b723b33ecc704e /subprojects/language-semantics/src | |
parent | chore: upgrade to Eclipse 2023-12 (diff) | |
download | refinery-d40ec70132ebb324873cb8c3868eb65309f46f8c.tar.gz refinery-d40ec70132ebb324873cb8c3868eb65309f46f8c.tar.zst refinery-d40ec70132ebb324873cb8c3868eb65309f46f8c.zip |
feat: state-based store for cross references
Efficiently store cross references even if default ref(*, *): false.
Uses propagation rules instead of view queries to reason about type constraints
and multiplicity.
Diffstat (limited to 'subprojects/language-semantics/src')
7 files changed, 77 insertions, 19 deletions
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java index ecaa7e0d..38bf5a61 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java | |||
@@ -27,9 +27,7 @@ import tools.refinery.store.reasoning.seed.ModelSeed; | |||
27 | import tools.refinery.store.reasoning.seed.Seed; | 27 | import tools.refinery.store.reasoning.seed.Seed; |
28 | import tools.refinery.store.reasoning.translator.TranslationException; | 28 | import tools.refinery.store.reasoning.translator.TranslationException; |
29 | import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; | 29 | import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; |
30 | import tools.refinery.store.reasoning.translator.metamodel.Metamodel; | 30 | import tools.refinery.store.reasoning.translator.metamodel.*; |
31 | import tools.refinery.store.reasoning.translator.metamodel.MetamodelBuilder; | ||
32 | import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator; | ||
33 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | 31 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; |
34 | import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; | 32 | import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; |
35 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | 33 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; |
@@ -73,6 +71,10 @@ public class ModelInitializer { | |||
73 | 71 | ||
74 | private ScopePropagator scopePropagator; | 72 | private ScopePropagator scopePropagator; |
75 | 73 | ||
74 | private int nodeCount; | ||
75 | |||
76 | private ModelSeed.Builder modelSeedBuilder; | ||
77 | |||
76 | private ModelSeed modelSeed; | 78 | private ModelSeed modelSeed; |
77 | 79 | ||
78 | public void readProblem(Problem problem) { | 80 | public void readProblem(Problem problem) { |
@@ -101,13 +103,17 @@ public class ModelInitializer { | |||
101 | TruthValue.FALSE)); | 103 | TruthValue.FALSE)); |
102 | collectNodes(); | 104 | collectNodes(); |
103 | collectPartialSymbols(); | 105 | collectPartialSymbols(); |
106 | nodeCount = problemTrace.getNodeTrace().size(); | ||
107 | modelSeedBuilder = ModelSeed.builder(nodeCount); | ||
108 | collectAssertions(); | ||
104 | collectMetamodel(); | 109 | collectMetamodel(); |
105 | metamodel = metamodelBuilder.build(); | 110 | metamodel = metamodelBuilder.build(); |
106 | problemTrace.setMetamodel(metamodel); | 111 | problemTrace.setMetamodel(metamodel); |
107 | collectAssertions(); | 112 | fixClassDeclarationAssertions(); |
108 | int nodeCount = problemTrace.getNodeTrace().size(); | ||
109 | var modelSeedBuilder = ModelSeed.builder(nodeCount); | ||
110 | for (var entry : relationInfoMap.entrySet()) { | 113 | for (var entry : relationInfoMap.entrySet()) { |
114 | if (entry.getKey() instanceof ReferenceDeclaration) { | ||
115 | continue; | ||
116 | } | ||
111 | var info = entry.getValue(); | 117 | var info = entry.getValue(); |
112 | var partialRelation = info.partialRelation(); | 118 | var partialRelation = info.partialRelation(); |
113 | modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount)); | 119 | modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount)); |
@@ -296,7 +302,20 @@ public class ModelInitializer { | |||
296 | } | 302 | } |
297 | var multiplicity = getMultiplicityConstraint(referenceDeclaration); | 303 | var multiplicity = getMultiplicityConstraint(referenceDeclaration); |
298 | try { | 304 | try { |
299 | metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation); | 305 | var seed = relationInfoMap.get(referenceDeclaration).toSeed(nodeCount); |
306 | var defaultValue = seed.majorityValue(); | ||
307 | if (defaultValue.must()) { | ||
308 | defaultValue = TruthValue.FALSE; | ||
309 | } | ||
310 | modelSeedBuilder.seed(relation, seed); | ||
311 | metamodelBuilder.reference(relation, ReferenceInfo.builder() | ||
312 | .containment(containment) | ||
313 | .source(source) | ||
314 | .multiplicity(multiplicity) | ||
315 | .target(target) | ||
316 | .opposite(oppositeRelation) | ||
317 | .defaultValue(defaultValue) | ||
318 | .build()); | ||
300 | } catch (RuntimeException e) { | 319 | } catch (RuntimeException e) { |
301 | throw TracedException.addTrace(classDeclaration, e); | 320 | throw TracedException.addTrace(classDeclaration, e); |
302 | } | 321 | } |
@@ -355,10 +374,6 @@ public class ModelInitializer { | |||
355 | collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN); | 374 | collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN); |
356 | var tuple = Tuple.of(newNodeId); | 375 | var tuple = Tuple.of(newNodeId); |
357 | mergeValue(classDeclaration, tuple, TruthValue.TRUE); | 376 | mergeValue(classDeclaration, tuple, TruthValue.TRUE); |
358 | var typeInfo = metamodel.typeHierarchy().getAnalysisResult(getPartialRelation(classDeclaration)); | ||
359 | for (var subType : typeInfo.getDirectSubtypes()) { | ||
360 | partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE); | ||
361 | } | ||
362 | } | 377 | } |
363 | 378 | ||
364 | private void collectEnumAssertions(EnumDeclaration enumDeclaration) { | 379 | private void collectEnumAssertions(EnumDeclaration enumDeclaration) { |
@@ -399,6 +414,27 @@ public class ModelInitializer { | |||
399 | } | 414 | } |
400 | } | 415 | } |
401 | 416 | ||
417 | private void fixClassDeclarationAssertions() { | ||
418 | for (var statement : problem.getStatements()) { | ||
419 | if (statement instanceof ClassDeclaration classDeclaration) { | ||
420 | fixClassDeclarationAssertions(classDeclaration); | ||
421 | } | ||
422 | } | ||
423 | } | ||
424 | |||
425 | private void fixClassDeclarationAssertions(ClassDeclaration classDeclaration) { | ||
426 | var newNode = classDeclaration.getNewNode(); | ||
427 | if (newNode == null) { | ||
428 | return; | ||
429 | } | ||
430 | var newNodeId = getNodeId(newNode); | ||
431 | var tuple = Tuple.of(newNodeId); | ||
432 | var typeInfo = metamodel.typeHierarchy().getAnalysisResult(getPartialRelation(classDeclaration)); | ||
433 | for (var subType : typeInfo.getDirectSubtypes()) { | ||
434 | partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE); | ||
435 | } | ||
436 | } | ||
437 | |||
402 | private void mergeValue(Relation relation, Tuple key, TruthValue value) { | 438 | private void mergeValue(Relation relation, Tuple key, TruthValue value) { |
403 | getRelationInfo(relation).assertions().mergeValue(key, value); | 439 | getRelationInfo(relation).assertions().mergeValue(key, value); |
404 | } | 440 | } |
@@ -482,7 +518,7 @@ public class ModelInitializer { | |||
482 | defaultValue = TruthValue.FALSE; | 518 | defaultValue = TruthValue.FALSE; |
483 | } else { | 519 | } else { |
484 | var seed = modelSeed.getSeed(partialRelation); | 520 | var seed = modelSeed.getSeed(partialRelation); |
485 | defaultValue = seed.reducedValue() == TruthValue.FALSE ? TruthValue.FALSE : TruthValue.UNKNOWN; | 521 | defaultValue = seed.majorityValue() == TruthValue.FALSE ? TruthValue.FALSE : TruthValue.UNKNOWN; |
486 | var cursor = seed.getCursor(defaultValue, problemTrace.getNodeTrace().size()); | 522 | var cursor = seed.getCursor(defaultValue, problemTrace.getNodeTrace().size()); |
487 | // The symbol should be mutable if there is at least one non-default entry in the seed. | 523 | // The symbol should be mutable if there is at least one non-default entry in the seed. |
488 | mutable = mutable || cursor.move(); | 524 | mutable = mutable || cursor.move(); |
@@ -495,7 +531,7 @@ public class ModelInitializer { | |||
495 | var problemParameters = predicateDefinition.getParameters(); | 531 | var problemParameters = predicateDefinition.getParameters(); |
496 | int arity = problemParameters.size(); | 532 | int arity = problemParameters.size(); |
497 | var parameters = new NodeVariable[arity]; | 533 | var parameters = new NodeVariable[arity]; |
498 | var parameterMap = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(arity); | 534 | var parameterMap = HashMap.<tools.refinery.language.model.problem.Variable, Variable>newHashMap(arity); |
499 | var commonLiterals = new ArrayList<Literal>(); | 535 | var commonLiterals = new ArrayList<Literal>(); |
500 | for (int i = 0; i < arity; i++) { | 536 | for (int i = 0; i < arity; i++) { |
501 | var problemParameter = problemParameters.get(i); | 537 | var problemParameter = problemParameters.get(i); |
@@ -532,7 +568,7 @@ public class ModelInitializer { | |||
532 | return existing; | 568 | return existing; |
533 | } | 569 | } |
534 | int localScopeSize = existing.size() + newVariables.size(); | 570 | int localScopeSize = existing.size() + newVariables.size(); |
535 | var localScope = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(localScopeSize); | 571 | var localScope = HashMap.<tools.refinery.language.model.problem.Variable, Variable>newHashMap(localScopeSize); |
536 | localScope.putAll(existing); | 572 | localScope.putAll(existing); |
537 | for (var newVariable : newVariables) { | 573 | for (var newVariable : newVariables) { |
538 | localScope.put(newVariable, Variable.of(newVariable.getName())); | 574 | localScope.put(newVariable, Variable.of(newVariable.getName())); |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java index c732f784..5d25f148 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java | |||
@@ -40,8 +40,8 @@ class DecisionTree implements MutableSeed<TruthValue> { | |||
40 | } | 40 | } |
41 | 41 | ||
42 | @Override | 42 | @Override |
43 | public TruthValue reducedValue() { | 43 | public TruthValue majorityValue() { |
44 | return root.getOtherwiseReducedValue().getTruthValue(); | 44 | return root.getMajorityValue().getTruthValueOrElse(TruthValue.FALSE); |
45 | } | 45 | } |
46 | 46 | ||
47 | @Override | 47 | @Override |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java index ebca2634..31d6fc78 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java | |||
@@ -100,6 +100,8 @@ abstract class DecisionTreeNode { | |||
100 | 100 | ||
101 | protected abstract LazyIntIterable getChildKeys(); | 101 | protected abstract LazyIntIterable getChildKeys(); |
102 | 102 | ||
103 | public abstract DecisionTreeValue getMajorityValue(); | ||
104 | |||
103 | protected abstract boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, | 105 | protected abstract boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, |
104 | int[] sortedChildren); | 106 | int[] sortedChildren); |
105 | 107 | ||
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java index 0e2f5d18..2ad216ce 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java | |||
@@ -130,6 +130,11 @@ final class IntermediateNode extends DecisionTreeNode { | |||
130 | return children.keysView(); | 130 | return children.keysView(); |
131 | } | 131 | } |
132 | 132 | ||
133 | @Override | ||
134 | public DecisionTreeValue getMajorityValue() { | ||
135 | return otherwise.getMajorityValue(); | ||
136 | } | ||
137 | |||
133 | protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) { | 138 | protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) { |
134 | for (int i = startIndex; i < sortedChildren.length; i++) { | 139 | for (int i = startIndex; i < sortedChildren.length; i++) { |
135 | var key = sortedChildren[i]; | 140 | var key = sortedChildren[i]; |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java index 7a72c656..f100c5a6 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java | |||
@@ -29,14 +29,14 @@ class NullaryMutableSeed implements MutableSeed<TruthValue> { | |||
29 | } | 29 | } |
30 | 30 | ||
31 | @Override | 31 | @Override |
32 | public TruthValue reducedValue() { | 32 | public TruthValue majorityValue() { |
33 | return value.getTruthValue(); | 33 | return value.getTruthValue(); |
34 | } | 34 | } |
35 | 35 | ||
36 | @Override | 36 | @Override |
37 | public TruthValue get(Tuple key) { | 37 | public TruthValue get(Tuple key) { |
38 | validateKey(key); | 38 | validateKey(key); |
39 | return reducedValue(); | 39 | return majorityValue(); |
40 | } | 40 | } |
41 | 41 | ||
42 | private static void validateKey(Tuple key) { | 42 | private static void validateKey(Tuple key) { |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java index d3dd757c..dc501479 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java | |||
@@ -115,7 +115,7 @@ class TerminalNode extends DecisionTreeNode { | |||
115 | 115 | ||
116 | @Override | 116 | @Override |
117 | protected DecisionTreeValue getOtherwiseReducedValue() { | 117 | protected DecisionTreeValue getOtherwiseReducedValue() { |
118 | return otherwise; | 118 | return getMajorityValue(); |
119 | } | 119 | } |
120 | 120 | ||
121 | @Override | 121 | @Override |
@@ -124,6 +124,11 @@ class TerminalNode extends DecisionTreeNode { | |||
124 | } | 124 | } |
125 | 125 | ||
126 | @Override | 126 | @Override |
127 | public DecisionTreeValue getMajorityValue() { | ||
128 | return otherwise; | ||
129 | } | ||
130 | |||
131 | @Override | ||
127 | protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) { | 132 | protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) { |
128 | if (startIndex >= sortedChildren.length) { | 133 | if (startIndex >= sortedChildren.length) { |
129 | return false; | 134 | return false; |
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java index 2320de2c..61ce850f 100644 --- a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java +++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java | |||
@@ -276,6 +276,16 @@ class DecisionTreeTests { | |||
276 | assertThat(sut.getReducedValue(), is(TruthValue.TRUE)); | 276 | assertThat(sut.getReducedValue(), is(TruthValue.TRUE)); |
277 | } | 277 | } |
278 | 278 | ||
279 | @Test | ||
280 | void overwriteWildcardAllTest() { | ||
281 | var first = new DecisionTree(2, TruthValue.UNKNOWN); | ||
282 | first.mergeValue(Tuple.of(-1, -1), TruthValue.FALSE); | ||
283 | var second = new DecisionTree(2, null); | ||
284 | second.mergeValue(Tuple.of(1, -1), TruthValue.TRUE); | ||
285 | first.overwriteValues(second); | ||
286 | assertThat(first.majorityValue(), is(TruthValue.FALSE)); | ||
287 | } | ||
288 | |||
279 | private Map<Tuple, TruthValue> iterateAll(DecisionTree sut, TruthValue defaultValue, int nodeCount) { | 289 | private Map<Tuple, TruthValue> iterateAll(DecisionTree sut, TruthValue defaultValue, int nodeCount) { |
280 | var cursor = sut.getCursor(defaultValue, nodeCount); | 290 | var cursor = sut.getCursor(defaultValue, nodeCount); |
281 | var map = new LinkedHashMap<Tuple, TruthValue>(); | 291 | var map = new LinkedHashMap<Tuple, TruthValue>(); |