aboutsummaryrefslogtreecommitdiffstats
path: root/subprojects/language-semantics/src/main/java
diff options
context:
space:
mode:
Diffstat (limited to 'subprojects/language-semantics/src/main/java')
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/BuiltInDetail.java10
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ClassDetail.java16
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/Metadata.java12
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/MetadataCreator.java181
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeKind.java12
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeMetadata.java9
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/OppositeReferenceDetail.java9
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/PredicateDetail.java16
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ReferenceDetail.java16
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationDetail.java10
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationMetadata.java9
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java665
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/SemanticsUtils.java31
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java51
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java32
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java9
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/MutableSeed.java28
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/NullaryMutableSeed.java83
18 files changed, 1151 insertions, 48 deletions
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/BuiltInDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/BuiltInDetail.java
new file mode 100644
index 00000000..6f706069
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/BuiltInDetail.java
@@ -0,0 +1,10 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public record BuiltInDetail() implements RelationDetail {
9 public static final BuiltInDetail INSTANCE = new BuiltInDetail();
10}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ClassDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ClassDetail.java
new file mode 100644
index 00000000..1d3190f5
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ClassDetail.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 */
6package tools.refinery.language.semantics.metadata;
7
8public record ClassDetail(boolean abstractClass) implements RelationDetail {
9 public static final ClassDetail CONCRETE_CLASS = new ClassDetail(false);
10
11 public static final ClassDetail ABSTRACT_CLASS = new ClassDetail(true);
12
13 public static ClassDetail ofAbstractClass(boolean abstractClass) {
14 return abstractClass ? ABSTRACT_CLASS : CONCRETE_CLASS;
15 }
16}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/Metadata.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/Metadata.java
new file mode 100644
index 00000000..d2dcb43a
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/Metadata.java
@@ -0,0 +1,12 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public sealed interface Metadata permits NodeMetadata, RelationMetadata {
9 String name();
10
11 String simpleName();
12}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/MetadataCreator.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/MetadataCreator.java
new file mode 100644
index 00000000..0c18b1b3
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/MetadataCreator.java
@@ -0,0 +1,181 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8import com.google.inject.Inject;
9import org.eclipse.emf.ecore.EObject;
10import org.eclipse.xtext.naming.IQualifiedNameConverter;
11import org.eclipse.xtext.naming.IQualifiedNameProvider;
12import org.eclipse.xtext.naming.QualifiedName;
13import org.eclipse.xtext.scoping.IScope;
14import org.eclipse.xtext.scoping.IScopeProvider;
15import tools.refinery.language.model.problem.*;
16import tools.refinery.language.semantics.model.ModelInitializer;
17import tools.refinery.language.semantics.model.TracedException;
18import tools.refinery.language.utils.ProblemUtil;
19import tools.refinery.store.reasoning.representation.PartialRelation;
20
21import java.util.*;
22
23public class MetadataCreator {
24 @Inject
25 private IScopeProvider scopeProvider;
26
27 @Inject
28 private IQualifiedNameProvider qualifiedNameProvider;
29
30 @Inject
31 private IQualifiedNameConverter qualifiedNameConverter;
32
33 private ModelInitializer initializer;
34
35 private IScope nodeScope;
36
37 private IScope relationScope;
38
39 public void setInitializer(ModelInitializer initializer) {
40 if (initializer == null) {
41 throw new IllegalArgumentException("Initializer was already set");
42 }
43 this.initializer = initializer;
44 var problem = initializer.getProblem();
45 nodeScope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE);
46 relationScope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION);
47 }
48
49 public List<NodeMetadata> getNodesMetadata() {
50 var nodes = new NodeMetadata[initializer.getNodeCount()];
51 for (var entry : initializer.getNodeTrace().keyValuesView()) {
52 var node = entry.getOne();
53 var id = entry.getTwo();
54 nodes[id] = getNodeMetadata(node);
55 }
56 return List.of(nodes);
57 }
58
59 private NodeMetadata getNodeMetadata(Node node) {
60 var qualifiedName = getQualifiedName(node);
61 var simpleName = getSimpleName(node, qualifiedName, nodeScope);
62 return new NodeMetadata(qualifiedNameConverter.toString(qualifiedName),
63 qualifiedNameConverter.toString(simpleName), getNodeKind(node));
64 }
65
66 private NodeKind getNodeKind(Node node) {
67 if (ProblemUtil.isImplicitNode(node)) {
68 return NodeKind.IMPLICIT;
69 } else if (ProblemUtil.isIndividualNode(node)) {
70 return NodeKind.INDIVIDUAL;
71 } else if (ProblemUtil.isNewNode(node)) {
72 return NodeKind.NEW;
73 } else {
74 throw new TracedException(node, "Unknown node type");
75 }
76 }
77
78 public List<RelationMetadata> getRelationsMetadata() {
79 var relationTrace = initializer.getRelationTrace();
80 var relations = new ArrayList<RelationMetadata>(relationTrace.size());
81 for (var entry : relationTrace.entrySet()) {
82 var relation = entry.getKey();
83 var partialRelation = entry.getValue();
84 var metadata = getRelationMetadata(relation, partialRelation);
85 relations.add(metadata);
86 }
87 return Collections.unmodifiableList(relations);
88 }
89
90 private RelationMetadata getRelationMetadata(Relation relation, PartialRelation partialRelation) {
91 var qualifiedName = getQualifiedName(relation);
92 var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
93 var simpleName = getSimpleName(relation, qualifiedName, relationScope);
94 var simpleNameString = qualifiedNameConverter.toString(simpleName);
95 var arity = partialRelation.arity();
96 var detail = getRelationDetail(relation, partialRelation);
97 return new RelationMetadata(qualifiedNameString, simpleNameString, arity, detail);
98 }
99
100 private RelationDetail getRelationDetail(Relation relation, PartialRelation partialRelation) {
101 if (ProblemUtil.isBuiltIn(relation) && !ProblemUtil.isError(relation)) {
102 return getBuiltInDetail();
103 }
104 if (relation instanceof ClassDeclaration classDeclaration) {
105 return getClassDetail(classDeclaration);
106 } else if (relation instanceof ReferenceDeclaration) {
107 return getReferenceDetail(partialRelation);
108 } else if (relation instanceof EnumDeclaration) {
109 return getEnumDetail();
110 } else if (relation instanceof PredicateDefinition predicateDefinition) {
111 return getPredicateDetail(predicateDefinition);
112 } else {
113 throw new TracedException(relation, "Unknown relation");
114 }
115 }
116
117 private RelationDetail getBuiltInDetail() {
118 return BuiltInDetail.INSTANCE;
119 }
120
121 private RelationDetail getClassDetail(ClassDeclaration classDeclaration) {
122 return ClassDetail.ofAbstractClass(classDeclaration.isAbstract());
123 }
124
125 private RelationDetail getReferenceDetail(PartialRelation partialRelation) {
126 var metamodel = initializer.getMetamodel();
127 var opposite = metamodel.oppositeReferences().get(partialRelation);
128 if (opposite == null) {
129 boolean isContainment = metamodel.containmentHierarchy().containsKey(partialRelation);
130 return ReferenceDetail.ofContainment(isContainment);
131 } else {
132 boolean isContainer = metamodel.containmentHierarchy().containsKey(opposite);
133 return new OppositeReferenceDetail(isContainer, opposite.name());
134 }
135 }
136
137 private RelationDetail getEnumDetail() {
138 return ClassDetail.CONCRETE_CLASS;
139 }
140
141 private RelationDetail getPredicateDetail(PredicateDefinition predicate) {
142 return PredicateDetail.ofError(predicate.isError());
143 }
144
145 private QualifiedName getQualifiedName(EObject eObject) {
146 var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(eObject);
147 if (qualifiedName == null) {
148 throw new TracedException(eObject, "Unknown qualified name");
149 }
150 return qualifiedName;
151 }
152
153 private QualifiedName getSimpleName(EObject eObject, QualifiedName qualifiedName, IScope scope) {
154 var descriptions = scope.getElements(eObject);
155 var names = new HashSet<QualifiedName>();
156 for (var description : descriptions) {
157 // {@code getQualifiedName()} will refer to the full name for objects that are loaded from the global
158 // scope, but {@code getName()} returns the qualified name that we set in
159 // {@code ProblemResourceDescriptionStrategy}.
160 names.add(description.getName());
161 }
162 var iterator = names.stream().sorted(Comparator.comparingInt(QualifiedName::getSegmentCount)).iterator();
163 while (iterator.hasNext()) {
164 var simpleName = iterator.next();
165 if (names.contains(simpleName) && isUnique(scope, simpleName)) {
166 return simpleName;
167 }
168 }
169 throw new TracedException(eObject, "Ambiguous qualified name: " +
170 qualifiedNameConverter.toString(qualifiedName));
171 }
172
173 private boolean isUnique(IScope scope, QualifiedName name) {
174 var iterator = scope.getElements(name).iterator();
175 if (!iterator.hasNext()) {
176 return false;
177 }
178 iterator.next();
179 return !iterator.hasNext();
180 }
181}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeKind.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeKind.java
new file mode 100644
index 00000000..01f0cd09
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeKind.java
@@ -0,0 +1,12 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public enum NodeKind {
9 IMPLICIT,
10 INDIVIDUAL,
11 NEW
12}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeMetadata.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeMetadata.java
new file mode 100644
index 00000000..812952c0
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeMetadata.java
@@ -0,0 +1,9 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public record NodeMetadata(String name, String simpleName, NodeKind kind) implements Metadata {
9}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/OppositeReferenceDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/OppositeReferenceDetail.java
new file mode 100644
index 00000000..26d7461c
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/OppositeReferenceDetail.java
@@ -0,0 +1,9 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public record OppositeReferenceDetail(boolean container, String opposite) implements RelationDetail {
9}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/PredicateDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/PredicateDetail.java
new file mode 100644
index 00000000..ca397eca
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/PredicateDetail.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 */
6package tools.refinery.language.semantics.metadata;
7
8public record PredicateDetail(boolean error) implements RelationDetail {
9 public static final PredicateDetail PREDICATE = new PredicateDetail(false);
10
11 public static final PredicateDetail ERROR_PREDICATE = new PredicateDetail(true);
12
13 public static PredicateDetail ofError(boolean error) {
14 return error ? ERROR_PREDICATE : PREDICATE;
15 }
16}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ReferenceDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ReferenceDetail.java
new file mode 100644
index 00000000..36771566
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ReferenceDetail.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 */
6package tools.refinery.language.semantics.metadata;
7
8public record ReferenceDetail(boolean containment) implements RelationDetail {
9 public static final ReferenceDetail CROSS_REFERENCE = new ReferenceDetail(false);
10
11 public static final ReferenceDetail CONTAINMENT_REFERENCE = new ReferenceDetail(true);
12
13 public static ReferenceDetail ofContainment(boolean containment) {
14 return containment ? CONTAINMENT_REFERENCE : CROSS_REFERENCE;
15 }
16}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationDetail.java
new file mode 100644
index 00000000..105179fd
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationDetail.java
@@ -0,0 +1,10 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public sealed interface RelationDetail permits ClassDetail, ReferenceDetail, PredicateDetail, OppositeReferenceDetail,
9 BuiltInDetail {
10}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationMetadata.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationMetadata.java
new file mode 100644
index 00000000..5abcc253
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationMetadata.java
@@ -0,0 +1,9 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public record RelationMetadata(String name, String simpleName, int arity, RelationDetail detail) implements Metadata {
9}
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 06b8ad77..89c41a8e 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
@@ -9,67 +9,399 @@ import com.google.inject.Inject;
9import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; 9import org.eclipse.collections.api.factory.primitive.ObjectIntMaps;
10import org.eclipse.collections.api.map.primitive.MutableObjectIntMap; 10import org.eclipse.collections.api.map.primitive.MutableObjectIntMap;
11import tools.refinery.language.model.problem.*; 11import tools.refinery.language.model.problem.*;
12import tools.refinery.language.semantics.model.internal.DecisionTree; 12import tools.refinery.language.semantics.model.internal.MutableSeed;
13import tools.refinery.language.utils.BuiltinSymbols;
13import tools.refinery.language.utils.ProblemDesugarer; 14import tools.refinery.language.utils.ProblemDesugarer;
14import tools.refinery.language.utils.RelationInfo; 15import tools.refinery.language.utils.ProblemUtil;
15import tools.refinery.store.representation.Symbol; 16import tools.refinery.store.model.ModelStoreBuilder;
17import tools.refinery.store.query.Constraint;
18import tools.refinery.store.query.dnf.InvalidClauseException;
19import tools.refinery.store.query.dnf.Query;
20import tools.refinery.store.query.dnf.RelationalQuery;
21import tools.refinery.store.query.literal.*;
22import tools.refinery.store.query.term.NodeVariable;
23import tools.refinery.store.query.term.Variable;
24import tools.refinery.store.reasoning.ReasoningAdapter;
25import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
26import tools.refinery.store.reasoning.representation.PartialRelation;
27import tools.refinery.store.reasoning.scope.ScopePropagatorBuilder;
28import tools.refinery.store.reasoning.seed.ModelSeed;
29import tools.refinery.store.reasoning.seed.Seed;
30import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
31import tools.refinery.store.reasoning.translator.metamodel.Metamodel;
32import tools.refinery.store.reasoning.translator.metamodel.MetamodelBuilder;
33import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator;
34import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
35import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
36import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
37import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMultiplicity;
38import tools.refinery.store.reasoning.translator.predicate.PredicateTranslator;
16import tools.refinery.store.representation.TruthValue; 39import tools.refinery.store.representation.TruthValue;
40import tools.refinery.store.representation.cardinality.CardinalityInterval;
41import tools.refinery.store.representation.cardinality.CardinalityIntervals;
42import tools.refinery.store.representation.cardinality.UpperCardinalities;
17import tools.refinery.store.tuple.Tuple; 43import tools.refinery.store.tuple.Tuple;
18 44
19import java.util.HashMap; 45import java.util.*;
20import java.util.Map;
21 46
22public class ModelInitializer { 47public class ModelInitializer {
23 @Inject 48 @Inject
24 private ProblemDesugarer desugarer; 49 private ProblemDesugarer desugarer;
25 50
51 @Inject
52 private SemanticsUtils semanticsUtils;
53
54 private Problem problem;
55
56 private ModelStoreBuilder storeBuilder;
57
58 private BuiltinSymbols builtinSymbols;
59
60 private PartialRelation nodeRelation;
61
26 private final MutableObjectIntMap<Node> nodeTrace = ObjectIntMaps.mutable.empty(); 62 private final MutableObjectIntMap<Node> nodeTrace = ObjectIntMaps.mutable.empty();
27 63
28 private final Map<tools.refinery.language.model.problem.Relation, Symbol<TruthValue>> relationTrace = 64 private final Map<Relation, RelationInfo> relationInfoMap = new LinkedHashMap<>();
29 new HashMap<>(); 65
66 private final Map<PartialRelation, RelationInfo> partialRelationInfoMap = new HashMap<>();
67
68 private final Map<AnyPartialSymbol, Relation> inverseTrace = new HashMap<>();
69
70 private Map<Relation, PartialRelation> relationTrace;
71
72 private final MetamodelBuilder metamodelBuilder = Metamodel.builder();
30 73
31 private int nodeCount = 0; 74 private Metamodel metamodel;
75
76 private Map<Tuple, CardinalityInterval> countSeed = new LinkedHashMap<>();
77
78 private ModelSeed modelSeed;
79
80 public Problem getProblem() {
81 return problem;
82 }
83
84 public int getNodeCount() {
85 return nodeTrace.size();
86 }
87
88 public MutableObjectIntMap<Node> getNodeTrace() {
89 return nodeTrace;
90 }
91
92 public Map<Relation, PartialRelation> getRelationTrace() {
93 return relationTrace;
94 }
32 95
33 public void createModel(Problem problem) { 96 public Relation getInverseTrace(AnyPartialSymbol partialRelation) {
34 var builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException( 97 return inverseTrace.get(partialRelation);
98 }
99
100 public Metamodel getMetamodel() {
101 return metamodel;
102 }
103
104 public ModelSeed createModel(Problem problem, ModelStoreBuilder storeBuilder) {
105 this.problem = problem;
106 this.storeBuilder = storeBuilder;
107 builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException(
35 "Problem has no builtin library")); 108 "Problem has no builtin library"));
36 var collectedSymbols = desugarer.collectSymbols(problem); 109 var nodeInfo = collectPartialRelation(builtinSymbols.node(), 1, TruthValue.TRUE, TruthValue.TRUE);
37 for (var node : collectedSymbols.nodes().keySet()) { 110 nodeRelation = nodeInfo.partialRelation();
38 nodeTrace.put(node, nodeCount); 111 metamodelBuilder.type(nodeRelation);
39 nodeCount += 1; 112 putRelationInfo(builtinSymbols.exists(), new RelationInfo(ReasoningAdapter.EXISTS_SYMBOL, null,
40 } 113 TruthValue.TRUE));
41 for (var pair : collectedSymbols.relations().entrySet()) { 114 putRelationInfo(builtinSymbols.equals(), new RelationInfo(ReasoningAdapter.EQUALS_SYMBOL,
42 var relation = pair.getKey(); 115 (TruthValue) null,
43 var relationInfo = pair.getValue(); 116 null));
44 var isEqualsRelation = relation == builtinSymbols.equals(); 117 putRelationInfo(builtinSymbols.contained(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINED_SYMBOL,
45 var decisionTree = mergeAssertions(relationInfo, isEqualsRelation); 118 null, TruthValue.UNKNOWN));
46 var defaultValue = isEqualsRelation ? TruthValue.FALSE : TruthValue.UNKNOWN; 119 putRelationInfo(builtinSymbols.contains(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINS_SYMBOL,
47 relationTrace.put(relation, Symbol.of( 120 null, TruthValue.UNKNOWN));
48 relationInfo.name(), relationInfo.arity(), TruthValue.class, defaultValue)); 121 putRelationInfo(builtinSymbols.invalidContainer(),
49 } 122 new RelationInfo(ContainmentHierarchyTranslator.INVALID_CONTAINER, TruthValue.FALSE,
50 } 123 TruthValue.FALSE));
51 124 collectNodes();
52 private DecisionTree mergeAssertions(RelationInfo relationInfo, boolean isEqualsRelation) { 125 collectPartialSymbols();
53 var arity = relationInfo.arity(); 126 collectMetamodel();
54 var defaultAssertions = new DecisionTree(arity, isEqualsRelation ? null : TruthValue.UNKNOWN); 127 metamodel = metamodelBuilder.build();
55 var assertions = new DecisionTree(arity); 128 collectAssertions();
56 for (var assertion : relationInfo.assertions()) { 129 storeBuilder.with(new MultiObjectTranslator());
57 var tuple = getTuple(assertion); 130 storeBuilder.with(new MetamodelTranslator(metamodel));
58 var value = getTruthValue(assertion.getValue()); 131 relationTrace = new LinkedHashMap<>(relationInfoMap.size());
59 if (assertion.isDefault()) { 132 int nodeCount = getNodeCount();
60 defaultAssertions.mergeValue(tuple, value); 133 var modelSeedBuilder = ModelSeed.builder(nodeCount);
134 for (var entry : relationInfoMap.entrySet()) {
135 var relation = entry.getKey();
136 var info = entry.getValue();
137 var partialRelation = info.partialRelation();
138 relationTrace.put(relation, partialRelation);
139 modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount));
140 }
141 collectScopes();
142 modelSeedBuilder.seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
143 .reducedValue(CardinalityIntervals.SET)
144 .putAll(countSeed));
145 modelSeed = modelSeedBuilder.build();
146 collectPredicates();
147 return modelSeed;
148 }
149
150 private void collectNodes() {
151 for (var statement : problem.getStatements()) {
152 if (statement instanceof IndividualDeclaration individualDeclaration) {
153 for (var individual : individualDeclaration.getNodes()) {
154 collectNode(individual);
155 }
156 } else if (statement instanceof ClassDeclaration classDeclaration) {
157 var newNode = classDeclaration.getNewNode();
158 if (newNode != null) {
159 collectNode(newNode);
160 }
161 } else if (statement instanceof EnumDeclaration enumDeclaration) {
162 for (var literal : enumDeclaration.getLiterals()) {
163 collectNode(literal);
164 }
165 }
166 }
167 for (var node : problem.getNodes()) {
168 collectNode(node);
169 }
170 }
171
172 private void collectNode(Node node) {
173 nodeTrace.getIfAbsentPut(node, this::getNodeCount);
174 }
175
176 private void collectPartialSymbols() {
177 for (var statement : problem.getStatements()) {
178 if (statement instanceof ClassDeclaration classDeclaration) {
179 collectClassDeclarationSymbols(classDeclaration);
180 } else if (statement instanceof EnumDeclaration enumDeclaration) {
181 collectPartialRelation(enumDeclaration, 1, TruthValue.FALSE, TruthValue.FALSE);
182 } else if (statement instanceof PredicateDefinition predicateDefinition) {
183 collectPredicateDefinitionSymbol(predicateDefinition);
184 }
185 }
186 }
187
188 private void collectClassDeclarationSymbols(ClassDeclaration classDeclaration) {
189 collectPartialRelation(classDeclaration, 1, null, TruthValue.UNKNOWN);
190 for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) {
191 if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) {
192 collectPartialRelation(referenceDeclaration, 2, null, TruthValue.UNKNOWN);
193 var invalidMultiplicityConstraint = referenceDeclaration.getInvalidMultiplicity();
194 if (invalidMultiplicityConstraint != null) {
195 collectPartialRelation(invalidMultiplicityConstraint, 1, TruthValue.FALSE, TruthValue.FALSE);
196 }
61 } else { 197 } else {
62 assertions.mergeValue(tuple, value); 198 throw new TracedException(featureDeclaration, "Unknown feature declaration");
199 }
200 }
201 }
202
203 private void collectPredicateDefinitionSymbol(PredicateDefinition predicateDefinition) {
204 int arity = predicateDefinition.getParameters().size();
205 if (predicateDefinition.isError()) {
206 collectPartialRelation(predicateDefinition, arity, TruthValue.FALSE, TruthValue.FALSE);
207 } else {
208 collectPartialRelation(predicateDefinition, arity, null, TruthValue.UNKNOWN);
209 }
210 }
211
212 private void putRelationInfo(Relation relation, RelationInfo info) {
213 relationInfoMap.put(relation, info);
214 partialRelationInfoMap.put(info.partialRelation(), info);
215 inverseTrace.put(info.partialRelation(), relation);
216 }
217
218 private RelationInfo collectPartialRelation(Relation relation, int arity, TruthValue value,
219 TruthValue defaultValue) {
220 return relationInfoMap.computeIfAbsent(relation, key -> {
221 var name = getName(relation);
222 var info = new RelationInfo(name, arity, value, defaultValue);
223 partialRelationInfoMap.put(info.partialRelation(), info);
224 inverseTrace.put(info.partialRelation(), relation);
225 return info;
226 });
227 }
228
229 private String getName(Relation relation) {
230 return semanticsUtils.getName(relation).orElseGet(() -> "#" + relationInfoMap.size());
231 }
232
233 private void collectMetamodel() {
234 for (var statement : problem.getStatements()) {
235 if (statement instanceof ClassDeclaration classDeclaration) {
236 collectClassDeclarationMetamodel(classDeclaration);
237 } else if (statement instanceof EnumDeclaration enumDeclaration) {
238 collectEnumMetamodel(enumDeclaration);
63 } 239 }
64 } 240 }
65 defaultAssertions.overwriteValues(assertions); 241 }
66 if (isEqualsRelation) { 242
67 for (int i = 0; i < nodeCount; i++) { 243 private void collectEnumMetamodel(EnumDeclaration enumDeclaration) {
68 defaultAssertions.setIfMissing(Tuple.of(i, i), TruthValue.TRUE); 244 try {
245 metamodelBuilder.type(getPartialRelation(enumDeclaration), nodeRelation);
246 } catch (RuntimeException e) {
247 throw TracedException.addTrace(enumDeclaration, e);
248 }
249 }
250
251 private void collectClassDeclarationMetamodel(ClassDeclaration classDeclaration) {
252 var superTypes = classDeclaration.getSuperTypes();
253 var partialSuperTypes = new ArrayList<PartialRelation>(superTypes.size() + 1);
254 partialSuperTypes.add(nodeRelation);
255 for (var superType : superTypes) {
256 partialSuperTypes.add(getPartialRelation(superType));
257 }
258 try {
259 metamodelBuilder.type(getPartialRelation(classDeclaration), classDeclaration.isAbstract(),
260 partialSuperTypes);
261 } catch (RuntimeException e) {
262 throw TracedException.addTrace(classDeclaration, e);
263 }
264 for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) {
265 if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) {
266 collectReferenceDeclarationMetamodel(classDeclaration, referenceDeclaration);
69 } 267 }
70 defaultAssertions.setAllMissing(TruthValue.FALSE);
71 } 268 }
72 return defaultAssertions; 269 }
270
271 private void collectReferenceDeclarationMetamodel(ClassDeclaration classDeclaration,
272 ReferenceDeclaration referenceDeclaration) {
273 var relation = getPartialRelation(referenceDeclaration);
274 var source = getPartialRelation(classDeclaration);
275 var target = getPartialRelation(referenceDeclaration.getReferenceType());
276 boolean containment = referenceDeclaration.getKind() == ReferenceKind.CONTAINMENT;
277 var opposite = referenceDeclaration.getOpposite();
278 PartialRelation oppositeRelation = null;
279 if (opposite != null) {
280 oppositeRelation = getPartialRelation(opposite);
281 }
282 var multiplicity = getMultiplicityConstraint(referenceDeclaration);
283 try {
284 metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation);
285 } catch (RuntimeException e) {
286 throw TracedException.addTrace(classDeclaration, e);
287 }
288 }
289
290 private Multiplicity getMultiplicityConstraint(ReferenceDeclaration referenceDeclaration) {
291 if (!ProblemUtil.hasMultiplicityConstraint(referenceDeclaration)) {
292 return UnconstrainedMultiplicity.INSTANCE;
293 }
294 var problemMultiplicity = referenceDeclaration.getMultiplicity();
295 CardinalityInterval interval;
296 if (problemMultiplicity == null) {
297 interval = CardinalityIntervals.LONE;
298 } else {
299 interval = getCardinalityInterval(problemMultiplicity);
300 }
301 var constraint = getRelationInfo(referenceDeclaration.getInvalidMultiplicity()).partialRelation();
302 return ConstrainedMultiplicity.of(interval, constraint);
303 }
304
305 private static CardinalityInterval getCardinalityInterval(
306 tools.refinery.language.model.problem.Multiplicity problemMultiplicity) {
307 if (problemMultiplicity instanceof ExactMultiplicity exactMultiplicity) {
308 return CardinalityIntervals.exactly(exactMultiplicity.getExactValue());
309 } else if (problemMultiplicity instanceof RangeMultiplicity rangeMultiplicity) {
310 var upperBound = rangeMultiplicity.getUpperBound();
311 return CardinalityIntervals.between(rangeMultiplicity.getLowerBound(),
312 upperBound < 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(upperBound));
313 } else {
314 throw new TracedException(problemMultiplicity, "Unknown multiplicity");
315 }
316 }
317
318 private void collectAssertions() {
319 for (var statement : problem.getStatements()) {
320 if (statement instanceof ClassDeclaration classDeclaration) {
321 collectClassDeclarationAssertions(classDeclaration);
322 } else if (statement instanceof EnumDeclaration enumDeclaration) {
323 collectEnumAssertions(enumDeclaration);
324 } else if (statement instanceof IndividualDeclaration individualDeclaration) {
325 for (var individual : individualDeclaration.getNodes()) {
326 collectIndividualAssertions(individual);
327 }
328 } else if (statement instanceof Assertion assertion) {
329 collectAssertion(assertion);
330 }
331 }
332 }
333
334 private void collectClassDeclarationAssertions(ClassDeclaration classDeclaration) {
335 var newNode = classDeclaration.getNewNode();
336 if (newNode == null) {
337 return;
338 }
339 var newNodeId = getNodeId(newNode);
340 collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN);
341 var tuple = Tuple.of(newNodeId);
342 mergeValue(classDeclaration, tuple, TruthValue.TRUE);
343 var typeInfo = metamodel.typeHierarchy().getAnalysisResult(getPartialRelation(classDeclaration));
344 for (var subType : typeInfo.getDirectSubtypes()) {
345 partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE);
346 }
347 }
348
349 private void collectEnumAssertions(EnumDeclaration enumDeclaration) {
350 var overlay = MutableSeed.of(1, null);
351 for (var literal : enumDeclaration.getLiterals()) {
352 collectIndividualAssertions(literal);
353 var nodeId = getNodeId(literal);
354 overlay.mergeValue(Tuple.of(nodeId), TruthValue.TRUE);
355 }
356 var info = getRelationInfo(enumDeclaration);
357 info.assertions().overwriteValues(overlay);
358 }
359
360 private void collectIndividualAssertions(Node node) {
361 var nodeId = getNodeId(node);
362 collectCardinalityAssertions(nodeId, TruthValue.TRUE);
363 }
364
365 private void collectCardinalityAssertions(int nodeId, TruthValue value) {
366 mergeValue(builtinSymbols.exists(), Tuple.of(nodeId), value);
367 mergeValue(builtinSymbols.equals(), Tuple.of(nodeId, nodeId), value);
368 }
369
370 private void collectAssertion(Assertion assertion) {
371 var tuple = getTuple(assertion);
372 var value = getTruthValue(assertion.getValue());
373 var relation = assertion.getRelation();
374 var info = getRelationInfo(relation);
375 var partialRelation = info.partialRelation();
376 if (partialRelation.arity() != tuple.getSize()) {
377 throw new TracedException(assertion, "Expected %d arguments for %s, got %d instead"
378 .formatted(partialRelation.arity(), partialRelation, tuple.getSize()));
379 }
380 if (assertion.isDefault()) {
381 info.defaultAssertions().mergeValue(tuple, value);
382 } else {
383 info.assertions().mergeValue(tuple, value);
384 }
385 }
386
387 private void mergeValue(Relation relation, Tuple key, TruthValue value) {
388 getRelationInfo(relation).assertions().mergeValue(key, value);
389 }
390
391 private RelationInfo getRelationInfo(Relation relation) {
392 var info = relationInfoMap.get(relation);
393 if (info == null) {
394 throw new IllegalArgumentException("Unknown relation: " + relation);
395 }
396 return info;
397 }
398
399 private PartialRelation getPartialRelation(Relation relation) {
400 return getRelationInfo(relation).partialRelation();
401 }
402
403 private int getNodeId(Node node) {
404 return nodeTrace.getOrThrow(node);
73 } 405 }
74 406
75 private Tuple getTuple(Assertion assertion) { 407 private Tuple getTuple(Assertion assertion) {
@@ -79,11 +411,11 @@ public class ModelInitializer {
79 for (int i = 0; i < arity; i++) { 411 for (int i = 0; i < arity; i++) {
80 var argument = arguments.get(i); 412 var argument = arguments.get(i);
81 if (argument instanceof NodeAssertionArgument nodeArgument) { 413 if (argument instanceof NodeAssertionArgument nodeArgument) {
82 nodes[i] = nodeTrace.getOrThrow(nodeArgument.getNode()); 414 nodes[i] = getNodeId(nodeArgument.getNode());
83 } else if (argument instanceof WildcardAssertionArgument) { 415 } else if (argument instanceof WildcardAssertionArgument) {
84 nodes[i] = -1; 416 nodes[i] = -1;
85 } else { 417 } else {
86 throw new IllegalArgumentException("Unknown assertion argument: " + argument); 418 throw new TracedException(argument, "Unsupported assertion argument");
87 } 419 }
88 } 420 }
89 return Tuple.of(nodes); 421 return Tuple.of(nodes);
@@ -100,4 +432,249 @@ public class ModelInitializer {
100 case ERROR -> TruthValue.ERROR; 432 case ERROR -> TruthValue.ERROR;
101 }; 433 };
102 } 434 }
435
436 private void collectPredicates() {
437 for (var statement : problem.getStatements()) {
438 if (statement instanceof PredicateDefinition predicateDefinition) {
439 collectPredicateDefinitionTraced(predicateDefinition);
440 }
441 }
442 }
443
444 private void collectPredicateDefinitionTraced(PredicateDefinition predicateDefinition) {
445 try {
446 collectPredicateDefinition(predicateDefinition);
447 } catch (InvalidClauseException e) {
448 int clauseIndex = e.getClauseIndex();
449 var bodies = predicateDefinition.getBodies();
450 if (clauseIndex < bodies.size()) {
451 throw new TracedException(bodies.get(clauseIndex), e);
452 } else {
453 throw new TracedException(predicateDefinition, e);
454 }
455 } catch (RuntimeException e) {
456 throw TracedException.addTrace(predicateDefinition, e);
457 }
458 }
459
460 private void collectPredicateDefinition(PredicateDefinition predicateDefinition) {
461 var partialRelation = getPartialRelation(predicateDefinition);
462 var query = toQuery(partialRelation.name(), predicateDefinition);
463 boolean mutable;
464 TruthValue defaultValue;
465 if (predicateDefinition.isError()) {
466 mutable = false;
467 defaultValue = TruthValue.FALSE;
468 } else {
469 var seed = modelSeed.getSeed(partialRelation);
470 defaultValue = seed.reducedValue() == TruthValue.FALSE ? TruthValue.FALSE : TruthValue.UNKNOWN;
471 var cursor = seed.getCursor(defaultValue, getNodeCount());
472 // The symbol should be mutable if there is at least one non-default entry in the seed.
473 mutable = cursor.move();
474 }
475 var translator = new PredicateTranslator(partialRelation, query, mutable, defaultValue);
476 storeBuilder.with(translator);
477 }
478
479 private RelationalQuery toQuery(String name, PredicateDefinition predicateDefinition) {
480 var problemParameters = predicateDefinition.getParameters();
481 int arity = problemParameters.size();
482 var parameters = new NodeVariable[arity];
483 var parameterMap = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(arity);
484 var commonLiterals = new ArrayList<Literal>();
485 for (int i = 0; i < arity; i++) {
486 var problemParameter = problemParameters.get(i);
487 var parameter = Variable.of(problemParameter.getName());
488 parameters[i] = parameter;
489 parameterMap.put(problemParameter, parameter);
490 var parameterType = problemParameter.getParameterType();
491 if (parameterType != null) {
492 var partialType = getPartialRelation(parameterType);
493 commonLiterals.add(partialType.call(parameter));
494 }
495 }
496 var builder = Query.builder(name).parameters(parameters);
497 for (var body : predicateDefinition.getBodies()) {
498 try {
499 var localScope = extendScope(parameterMap, body.getImplicitVariables());
500 var problemLiterals = body.getLiterals();
501 var literals = new ArrayList<>(commonLiterals);
502 for (var problemLiteral : problemLiterals) {
503 toLiteralsTraced(problemLiteral, localScope, literals);
504 }
505 builder.clause(literals);
506 } catch (RuntimeException e) {
507 throw TracedException.addTrace(body, e);
508 }
509 }
510 return builder.build();
511 }
512
513 private Map<tools.refinery.language.model.problem.Variable, Variable> extendScope(
514 Map<tools.refinery.language.model.problem.Variable, Variable> existing,
515 Collection<? extends tools.refinery.language.model.problem.Variable> newVariables) {
516 if (newVariables.isEmpty()) {
517 return existing;
518 }
519 int localScopeSize = existing.size() + newVariables.size();
520 var localScope = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(localScopeSize);
521 localScope.putAll(existing);
522 for (var newVariable : newVariables) {
523 localScope.put(newVariable, Variable.of(newVariable.getName()));
524 }
525 return localScope;
526 }
527
528 private void toLiteralsTraced(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope,
529 List<Literal> literals) {
530 try {
531 toLiterals(expr, localScope, literals);
532 } catch (RuntimeException e) {
533 throw TracedException.addTrace(expr, e);
534 }
535 }
536
537 private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable,
538 Variable> localScope,
539 List<Literal> literals) {
540 if (expr instanceof LogicConstant logicConstant) {
541 switch (logicConstant.getLogicValue()) {
542 case TRUE -> literals.add(BooleanLiteral.TRUE);
543 case FALSE -> literals.add(BooleanLiteral.FALSE);
544 default -> throw new TracedException(logicConstant, "Unsupported literal");
545 }
546 } else if (expr instanceof Atom atom) {
547 var target = getPartialRelation(atom.getRelation());
548 var polarity = atom.isTransitiveClosure() ? CallPolarity.TRANSITIVE : CallPolarity.POSITIVE;
549 var argumentList = toArgumentList(atom.getArguments(), localScope, literals);
550 literals.add(target.call(polarity, argumentList));
551 } else if (expr instanceof NegationExpr negationExpr) {
552 var body = negationExpr.getBody();
553 if (!(body instanceof Atom atom)) {
554 throw new TracedException(body, "Cannot negate literal");
555 }
556 var target = getPartialRelation(atom.getRelation());
557 Constraint constraint;
558 if (atom.isTransitiveClosure()) {
559 constraint = Query.of(target.name() + "#transitive", (builder, p1, p2) -> builder.clause(
560 target.callTransitive(p1, p2)
561 )).getDnf();
562 } else {
563 constraint = target;
564 }
565 var negatedScope = extendScope(localScope, negationExpr.getImplicitVariables());
566 var argumentList = toArgumentList(atom.getArguments(), negatedScope, literals);
567 literals.add(constraint.call(CallPolarity.NEGATIVE, argumentList));
568 } else if (expr instanceof ComparisonExpr comparisonExpr) {
569 var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()),
570 localScope, literals);
571 boolean positive = switch (comparisonExpr.getOp()) {
572 case EQ -> true;
573 case NOT_EQ -> false;
574 default -> throw new TracedException(
575 comparisonExpr, "Unsupported operator");
576 };
577 literals.add(new EquivalenceLiteral(positive, argumentList.get(0), argumentList.get(1)));
578 } else {
579 throw new TracedException(expr, "Unsupported literal");
580 }
581 }
582
583 private List<Variable> toArgumentList(
584 List<Expr> expressions, Map<tools.refinery.language.model.problem.Variable, Variable> localScope,
585 List<Literal> literals) {
586 var argumentList = new ArrayList<Variable>(expressions.size());
587 for (var expr : expressions) {
588 if (!(expr instanceof VariableOrNodeExpr variableOrNodeExpr)) {
589 throw new TracedException(expr, "Unsupported argument");
590 }
591 var variableOrNode = variableOrNodeExpr.getVariableOrNode();
592 if (variableOrNode instanceof Node node) {
593 int nodeId = getNodeId(node);
594 var tempVariable = Variable.of(semanticsUtils.getName(node).orElse("_" + nodeId));
595 literals.add(new ConstantLiteral(tempVariable, nodeId));
596 argumentList.add(tempVariable);
597 } else if (variableOrNode instanceof tools.refinery.language.model.problem.Variable problemVariable) {
598 if (variableOrNodeExpr.getSingletonVariable() == problemVariable) {
599 argumentList.add(Variable.of(problemVariable.getName()));
600 } else {
601 var variable = localScope.get(problemVariable);
602 if (variable == null) {
603 throw new TracedException(variableOrNode, "Unknown variable: " + problemVariable.getName());
604 }
605 argumentList.add(variable);
606 }
607 } else {
608 throw new TracedException(variableOrNode, "Unknown argument");
609 }
610 }
611 return argumentList;
612 }
613
614 private void collectScopes() {
615 for (var statement : problem.getStatements()) {
616 if (statement instanceof ScopeDeclaration scopeDeclaration) {
617 for (var typeScope : scopeDeclaration.getTypeScopes()) {
618 if (typeScope.isIncrement()) {
619 collectTypeScopeIncrement(typeScope);
620 } else {
621 collectTypeScope(typeScope);
622 }
623 }
624 }
625 }
626 }
627
628 private void collectTypeScopeIncrement(TypeScope typeScope) {
629 if (!(typeScope.getTargetType() instanceof ClassDeclaration classDeclaration)) {
630 throw new TracedException(typeScope, "Target of incremental type scope must be a class declaration");
631 }
632 var newNode = classDeclaration.getNewNode();
633 if (newNode == null) {
634 throw new TracedException(typeScope, "Target of incremental type scope must be concrete class");
635 }
636 int newNodeId = nodeTrace.get(newNode);
637 var type = relationTrace.get(classDeclaration);
638 var typeInfo = metamodel.typeHierarchy().getAnalysisResult(type);
639 if (!typeInfo.getDirectSubtypes().isEmpty()) {
640 throw new TracedException(typeScope, "Target of incremental type scope cannot have any subclasses");
641 }
642 var interval = getCardinalityInterval(typeScope.getMultiplicity());
643 countSeed.compute(Tuple.of(newNodeId), (key, oldValue) ->
644 oldValue == null ? interval : oldValue.meet(interval));
645 }
646
647 private void collectTypeScope(TypeScope typeScope) {
648 var scopePropagatorBuilder = storeBuilder.tryGetAdapter(ScopePropagatorBuilder.class).orElseThrow(
649 () -> new TracedException(typeScope, "Type scopes require a ScopePropagatorBuilder"));
650 var type = relationTrace.get(typeScope.getTargetType());
651 if (type == null) {
652 throw new TracedException(typeScope, "Unknown target type");
653 }
654 var interval = getCardinalityInterval(typeScope.getMultiplicity());
655 scopePropagatorBuilder.scope(type, interval);
656 }
657
658 private record RelationInfo(PartialRelation partialRelation, MutableSeed<TruthValue> assertions,
659 MutableSeed<TruthValue> defaultAssertions) {
660 public RelationInfo(String name, int arity, TruthValue value, TruthValue defaultValue) {
661 this(new PartialRelation(name, arity), value, defaultValue);
662 }
663
664 public RelationInfo(PartialRelation partialRelation, TruthValue value, TruthValue defaultValue) {
665 this(partialRelation, MutableSeed.of(partialRelation.arity(), value),
666 MutableSeed.of(partialRelation.arity(), defaultValue));
667 }
668
669 public Seed<TruthValue> toSeed(int nodeCount) {
670 defaultAssertions.overwriteValues(assertions);
671 if (partialRelation.equals(ReasoningAdapter.EQUALS_SYMBOL)) {
672 for (int i = 0; i < nodeCount; i++) {
673 defaultAssertions.setIfMissing(Tuple.of(i, i), TruthValue.TRUE);
674 }
675 defaultAssertions.setAllMissing(TruthValue.FALSE);
676 }
677 return defaultAssertions;
678 }
679 }
103} 680}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/SemanticsUtils.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/SemanticsUtils.java
new file mode 100644
index 00000000..47c89e9b
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/SemanticsUtils.java
@@ -0,0 +1,31 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.model;
7
8import com.google.inject.Inject;
9import com.google.inject.Singleton;
10import org.eclipse.emf.ecore.EObject;
11import org.eclipse.xtext.naming.IQualifiedNameConverter;
12import org.eclipse.xtext.naming.IQualifiedNameProvider;
13
14import java.util.Optional;
15
16@Singleton
17public class SemanticsUtils {
18 @Inject
19 private IQualifiedNameProvider qualifiedNameProvider;
20
21 @Inject
22 private IQualifiedNameConverter qualifiedNameConverter;
23
24 public Optional<String> getName(EObject eObject) {
25 var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(eObject);
26 if (qualifiedName == null) {
27 return Optional.empty();
28 }
29 return Optional.of(qualifiedNameConverter.toString(qualifiedName));
30 }
31}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java
new file mode 100644
index 00000000..38fd8a67
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java
@@ -0,0 +1,51 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.model;
7
8import org.eclipse.emf.ecore.EObject;
9
10public class TracedException extends RuntimeException {
11 private final transient EObject sourceElement;
12
13 public TracedException(EObject sourceElement) {
14 this.sourceElement = sourceElement;
15 }
16
17 public TracedException(EObject sourceElement, String message) {
18 super(message);
19 this.sourceElement = sourceElement;
20 }
21
22 public TracedException(EObject sourceElement, String message, Throwable cause) {
23 super(message, cause);
24 this.sourceElement = sourceElement;
25 }
26
27 public TracedException(EObject sourceElement, Throwable cause) {
28 super(cause);
29 this.sourceElement = sourceElement;
30 }
31
32 public EObject getSourceElement() {
33 return sourceElement;
34 }
35
36 @Override
37 public String getMessage() {
38 var message = super.getMessage();
39 if (message == null) {
40 return "Internal error";
41 }
42 return message;
43 }
44
45 public static TracedException addTrace(EObject sourceElement, Throwable cause) {
46 if (cause instanceof TracedException tracedException && tracedException.sourceElement != null) {
47 return tracedException;
48 }
49 return new TracedException(sourceElement, cause);
50 }
51}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java
index c1afecf9..32112e61 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java
@@ -7,10 +7,10 @@ package tools.refinery.language.semantics.model.internal;
7 7
8import org.eclipse.collections.api.factory.primitive.IntObjectMaps; 8import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
9import tools.refinery.store.map.Cursor; 9import tools.refinery.store.map.Cursor;
10import tools.refinery.store.tuple.Tuple;
11import tools.refinery.store.representation.TruthValue; 10import tools.refinery.store.representation.TruthValue;
11import tools.refinery.store.tuple.Tuple;
12 12
13public class DecisionTree { 13class DecisionTree implements MutableSeed<TruthValue> {
14 private final int levels; 14 private final int levels;
15 15
16 private final DecisionTreeNode root; 16 private final DecisionTreeNode root;
@@ -29,30 +29,53 @@ public class DecisionTree {
29 this(levels, null); 29 this(levels, null);
30 } 30 }
31 31
32 @Override
33 public int arity() {
34 return levels;
35 }
36
37 @Override
38 public Class<TruthValue> valueType() {
39 return TruthValue.class;
40 }
41
42 @Override
43 public TruthValue reducedValue() {
44 return root.getOtherwiseReducedValue().getTruthValue();
45 }
46
47 @Override
32 public TruthValue get(Tuple tuple) { 48 public TruthValue get(Tuple tuple) {
33 return root.getValue(levels - 1, tuple).getTruthValue(); 49 return root.getValue(levels - 1, tuple).getTruthValue();
34 } 50 }
35 51
52 @Override
36 public void mergeValue(Tuple tuple, TruthValue truthValue) { 53 public void mergeValue(Tuple tuple, TruthValue truthValue) {
37 if (truthValue != null) { 54 if (truthValue != null) {
38 root.mergeValue(levels - 1, tuple, truthValue); 55 root.mergeValue(levels - 1, tuple, truthValue);
39 } 56 }
40 } 57 }
41 58
59 @Override
42 public void setIfMissing(Tuple tuple, TruthValue truthValue) { 60 public void setIfMissing(Tuple tuple, TruthValue truthValue) {
43 if (truthValue != null) { 61 if (truthValue != null) {
44 root.setIfMissing(levels - 1, tuple, truthValue); 62 root.setIfMissing(levels - 1, tuple, truthValue);
45 } 63 }
46 } 64 }
47 65
66 @Override
48 public void setAllMissing(TruthValue truthValue) { 67 public void setAllMissing(TruthValue truthValue) {
49 if (truthValue != null) { 68 if (truthValue != null) {
50 root.setAllMissing(truthValue); 69 root.setAllMissing(truthValue);
51 } 70 }
52 } 71 }
53 72
54 public void overwriteValues(DecisionTree values) { 73 @Override
55 root.overwriteValues(values.root); 74 public void overwriteValues(MutableSeed<TruthValue> values) {
75 if (!(values instanceof DecisionTree decisionTree)) {
76 throw new IllegalArgumentException("Incompatible overwrite: " + values);
77 }
78 root.overwriteValues(decisionTree.root);
56 } 79 }
57 80
58 public TruthValue getReducedValue() { 81 public TruthValue getReducedValue() {
@@ -60,6 +83,7 @@ public class DecisionTree {
60 return reducedValue == null ? null : reducedValue.getTruthValue(); 83 return reducedValue == null ? null : reducedValue.getTruthValue();
61 } 84 }
62 85
86 @Override
63 public Cursor<Tuple, TruthValue> getCursor(TruthValue defaultValue, int nodeCount) { 87 public Cursor<Tuple, TruthValue> getCursor(TruthValue defaultValue, int nodeCount) {
64 return new DecisionTreeCursor(levels, defaultValue, nodeCount, root); 88 return new DecisionTreeCursor(levels, defaultValue, nodeCount, root);
65 } 89 }
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java
index 9a1e15a3..a9fc644a 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java
@@ -67,6 +67,15 @@ class DecisionTreeCursor implements Cursor<Tuple, TruthValue> {
67 67
68 @Override 68 @Override
69 public boolean move() { 69 public boolean move() {
70 while (moveOne()) {
71 if (!value.equals(defaultValue)) {
72 return true;
73 }
74 }
75 return false;
76 }
77
78 private boolean moveOne() {
70 boolean found = false; 79 boolean found = false;
71 if (path.isEmpty() && !terminated) { 80 if (path.isEmpty() && !terminated) {
72 found = root.moveNext(levels - 1, this); 81 found = root.moveNext(levels - 1, this);
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/MutableSeed.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/MutableSeed.java
new file mode 100644
index 00000000..99019e2a
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/MutableSeed.java
@@ -0,0 +1,28 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.model.internal;
7
8import tools.refinery.store.reasoning.seed.Seed;
9import tools.refinery.store.representation.TruthValue;
10import tools.refinery.store.tuple.Tuple;
11
12public interface MutableSeed<T> extends Seed<T> {
13 void mergeValue(Tuple tuple, T value);
14
15 void setIfMissing(Tuple tuple, T value);
16
17 void setAllMissing(T value);
18
19 void overwriteValues(MutableSeed<T> other);
20
21 static MutableSeed<TruthValue> of(int levels, TruthValue initialValue) {
22 if (levels == 0) {
23 return new NullaryMutableSeed(initialValue);
24 } else {
25 return new DecisionTree(levels, initialValue);
26 }
27 }
28}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/NullaryMutableSeed.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/NullaryMutableSeed.java
new file mode 100644
index 00000000..80644b1f
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/NullaryMutableSeed.java
@@ -0,0 +1,83 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.model.internal;
7
8import tools.refinery.store.map.Cursor;
9import tools.refinery.store.map.Cursors;
10import tools.refinery.store.representation.TruthValue;
11import tools.refinery.store.tuple.Tuple;
12
13class NullaryMutableSeed implements MutableSeed<TruthValue> {
14 private DecisionTreeValue value;
15
16 public NullaryMutableSeed(TruthValue reducedValue) {
17
18 value = DecisionTreeValue.fromTruthValue(reducedValue);
19 }
20
21 @Override
22 public int arity() {
23 return 0;
24 }
25
26 @Override
27 public Class<TruthValue> valueType() {
28 return TruthValue.class;
29 }
30
31 @Override
32 public TruthValue reducedValue() {
33 return value.getTruthValue();
34 }
35
36 @Override
37 public TruthValue get(Tuple key) {
38 validateKey(key);
39 return reducedValue();
40 }
41
42 private static void validateKey(Tuple key) {
43 if (key.getSize() > 0) {
44 throw new IllegalArgumentException("Invalid key: " + key);
45 }
46 }
47
48 @Override
49 public Cursor<Tuple, TruthValue> getCursor(TruthValue defaultValue, int nodeCount) {
50 if (value == DecisionTreeValue.UNSET || value.getTruthValue() == defaultValue) {
51 return Cursors.empty();
52 }
53 return Cursors.singleton(Tuple.of(), value.getTruthValue());
54 }
55
56 @Override
57 public void mergeValue(Tuple tuple, TruthValue value) {
58 this.value = DecisionTreeValue.fromTruthValue(this.value.merge(value));
59 }
60
61 @Override
62 public void setIfMissing(Tuple tuple, TruthValue value) {
63 validateKey(tuple);
64 setAllMissing(value);
65 }
66
67 @Override
68 public void setAllMissing(TruthValue value) {
69 if (this.value == DecisionTreeValue.UNSET) {
70 this.value = DecisionTreeValue.fromTruthValue(value);
71 }
72 }
73
74 @Override
75 public void overwriteValues(MutableSeed<TruthValue> other) {
76 if (!(other instanceof NullaryMutableSeed nullaryMutableSeed)) {
77 throw new IllegalArgumentException("Incompatible overwrite: " + other);
78 }
79 if (nullaryMutableSeed.value != DecisionTreeValue.UNSET) {
80 value = nullaryMutableSeed.value;
81 }
82 }
83}
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-09-08 22:01:03 +0000