diff options
author | Kristóf Marussy <kristof@marussy.com> | 2022-10-30 19:27:34 -0400 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2022-11-05 19:41:17 +0100 |
commit | 960af83c7c1cb871da03b9ac4ec6f44c94e78a1d (patch) | |
tree | 7d37ee007ee2d3b031d62ca892920d326758f438 /subprojects/language/src/main | |
parent | refactor: DNF query builder (diff) | |
download | refinery-960af83c7c1cb871da03b9ac4ec6f44c94e78a1d.tar.gz refinery-960af83c7c1cb871da03b9ac4ec6f44c94e78a1d.tar.zst refinery-960af83c7c1cb871da03b9ac4ec6f44c94e78a1d.zip |
refactor: DNF atoms
Restore count != capability.
Still needs semantics and tests for count atoms over partial models.
Diffstat (limited to 'subprojects/language/src/main')
3 files changed, 45 insertions, 33 deletions
diff --git a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext index f514e96c..2a8429a3 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext +++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext | |||
@@ -72,7 +72,7 @@ NegativeLiteral: | |||
72 | modality=Modality? "!" atom=Atom; | 72 | modality=Modality? "!" atom=Atom; |
73 | 73 | ||
74 | enum ComparisonOp: | 74 | enum ComparisonOp: |
75 | LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="=="; | 75 | LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="==" | NOT_EQ="!="; |
76 | 76 | ||
77 | CountLiteral: | 77 | CountLiteral: |
78 | modality=Modality? "count" atom=Atom op=ComparisonOp threshold=INT; | 78 | modality=Modality? "count" atom=Atom op=ComparisonOp threshold=INT; |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/RelationInfo.java b/subprojects/language/src/main/java/tools/refinery/language/utils/RelationInfo.java index ae56e3a5..2253d257 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/utils/RelationInfo.java +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/RelationInfo.java | |||
@@ -1,27 +1,24 @@ | |||
1 | package tools.refinery.language.utils; | 1 | package tools.refinery.language.utils; |
2 | 2 | ||
3 | import tools.refinery.language.model.problem.*; | ||
4 | |||
3 | import java.util.ArrayList; | 5 | import java.util.ArrayList; |
4 | import java.util.Collection; | 6 | import java.util.Collection; |
5 | import java.util.List; | 7 | import java.util.List; |
6 | 8 | ||
7 | import tools.refinery.language.model.problem.Assertion; | 9 | public record RelationInfo(String name, ContainmentRole containmentRole, List<Parameter> parameters, |
8 | import tools.refinery.language.model.problem.Conjunction; | 10 | Multiplicity multiplicity, Relation opposite, Collection<Conjunction> bodies, |
9 | import tools.refinery.language.model.problem.Multiplicity; | 11 | Collection<Assertion> assertions, Collection<TypeScope> typeScopes) { |
10 | import tools.refinery.language.model.problem.Parameter; | 12 | public RelationInfo(String name, ContainmentRole containmentRole, List<Parameter> parameters, |
11 | import tools.refinery.language.model.problem.PredicateKind; | 13 | Multiplicity multiplicity, Relation opposite, Collection<Conjunction> bodies) { |
12 | import tools.refinery.language.model.problem.Relation; | 14 | this(name, containmentRole, parameters, multiplicity, opposite, bodies, new ArrayList<>(), new ArrayList<>()); |
13 | import tools.refinery.language.model.problem.TypeScope; | ||
14 | |||
15 | public record RelationInfo(String name, PredicateKind kind, List<Parameter> parameters, Multiplicity multiplicity, | ||
16 | Relation opposite, Collection<Conjunction> bodies, Collection<Assertion> defaultAssertions, | ||
17 | Collection<Assertion> assertions, Collection<TypeScope> typeScopes) { | ||
18 | public RelationInfo(String name, PredicateKind kind, List<Parameter> parameters, Multiplicity multiplicity, | ||
19 | Relation opposite, Collection<Conjunction> bodies) { | ||
20 | this(name, kind, parameters, multiplicity, opposite, bodies, new ArrayList<>(), new ArrayList<>(), | ||
21 | new ArrayList<>()); | ||
22 | } | 15 | } |
23 | 16 | ||
24 | public boolean hasDefinition() { | 17 | public boolean hasDefinition() { |
25 | return bodies != null && !bodies.isEmpty(); | 18 | return bodies != null && !bodies.isEmpty(); |
26 | } | 19 | } |
20 | |||
21 | public int arity() { | ||
22 | return parameters.size(); | ||
23 | } | ||
27 | } | 24 | } |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java b/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java index a386db7f..210e96ab 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java | |||
@@ -19,10 +19,12 @@ class SymbolCollector { | |||
19 | private IQualifiedNameConverter qualifiedNameConverter; | 19 | private IQualifiedNameConverter qualifiedNameConverter; |
20 | 20 | ||
21 | @Inject | 21 | @Inject |
22 | ProblemDesugarer desugarer; | 22 | private ProblemDesugarer desugarer; |
23 | 23 | ||
24 | private BuiltinSymbols builtinSymbols; | 24 | private BuiltinSymbols builtinSymbols; |
25 | |||
25 | private final Map<Node, NodeInfo> nodes = new LinkedHashMap<>(); | 26 | private final Map<Node, NodeInfo> nodes = new LinkedHashMap<>(); |
27 | |||
26 | private final Map<Relation, RelationInfo> relations = new LinkedHashMap<>(); | 28 | private final Map<Relation, RelationInfo> relations = new LinkedHashMap<>(); |
27 | 29 | ||
28 | public CollectedSymbols collectSymbols(Problem problem) { | 30 | public CollectedSymbols collectSymbols(Problem problem) { |
@@ -54,9 +56,10 @@ class SymbolCollector { | |||
54 | } | 56 | } |
55 | 57 | ||
56 | private void collectPredicate(PredicateDefinition predicateDefinition) { | 58 | private void collectPredicate(PredicateDefinition predicateDefinition) { |
59 | var predicateKind = predicateDefinition.getKind(); | ||
57 | var info = new RelationInfo(getQualifiedNameString(predicateDefinition), | 60 | var info = new RelationInfo(getQualifiedNameString(predicateDefinition), |
58 | predicateDefinition.getKind(), | 61 | ContainmentRole.fromPredicateKind(predicateKind), predicateDefinition.getParameters(), null, null, |
59 | predicateDefinition.getParameters(), null, null, predicateDefinition.getBodies()); | 62 | predicateDefinition.getBodies()); |
60 | relations.put(predicateDefinition, info); | 63 | relations.put(predicateDefinition, info); |
61 | } | 64 | } |
62 | 65 | ||
@@ -65,10 +68,10 @@ class SymbolCollector { | |||
65 | // contained, including data types. | 68 | // contained, including data types. |
66 | var contained = | 69 | var contained = |
67 | classDeclaration != builtinSymbols.node() && classDeclaration != builtinSymbols.domain(); | 70 | classDeclaration != builtinSymbols.node() && classDeclaration != builtinSymbols.domain(); |
68 | var classKind = contained ? PredicateKind.CONTAINED : PredicateKind.DEFAULT; | 71 | var containmentRole = contained ? ContainmentRole.CONTAINED : ContainmentRole.NONE; |
69 | var instanceParameter = ProblemFactory.eINSTANCE.createParameter(); | 72 | var instanceParameter = ProblemFactory.eINSTANCE.createParameter(); |
70 | instanceParameter.setName("instance"); | 73 | instanceParameter.setName("instance"); |
71 | var classInfo = new RelationInfo(getQualifiedNameString(classDeclaration), classKind, | 74 | var classInfo = new RelationInfo(getQualifiedNameString(classDeclaration), containmentRole, |
72 | List.of(instanceParameter), null, null, List.of()); | 75 | List.of(instanceParameter), null, null, List.of()); |
73 | relations.put(classDeclaration, classInfo); | 76 | relations.put(classDeclaration, classInfo); |
74 | collectReferences(classDeclaration); | 77 | collectReferences(classDeclaration); |
@@ -76,9 +79,9 @@ class SymbolCollector { | |||
76 | 79 | ||
77 | private void collectReferences(ClassDeclaration classDeclaration) { | 80 | private void collectReferences(ClassDeclaration classDeclaration) { |
78 | for (var referenceDeclaration : classDeclaration.getReferenceDeclarations()) { | 81 | for (var referenceDeclaration : classDeclaration.getReferenceDeclarations()) { |
79 | var referenceKind = desugarer.isContainmentReference(referenceDeclaration) ? | 82 | var referenceRole = desugarer.isContainmentReference(referenceDeclaration) ? |
80 | PredicateKind.CONTAINMENT : | 83 | ContainmentRole.CONTAINMENT : |
81 | PredicateKind.DEFAULT; | 84 | ContainmentRole.NONE; |
82 | var sourceParameter = ProblemFactory.eINSTANCE.createParameter(); | 85 | var sourceParameter = ProblemFactory.eINSTANCE.createParameter(); |
83 | sourceParameter.setName("source"); | 86 | sourceParameter.setName("source"); |
84 | sourceParameter.setParameterType(classDeclaration); | 87 | sourceParameter.setParameterType(classDeclaration); |
@@ -91,7 +94,7 @@ class SymbolCollector { | |||
91 | multiplicity = exactMultiplicity; | 94 | multiplicity = exactMultiplicity; |
92 | } | 95 | } |
93 | targetParameter.setParameterType(referenceDeclaration.getReferenceType()); | 96 | targetParameter.setParameterType(referenceDeclaration.getReferenceType()); |
94 | var referenceInfo = new RelationInfo(getQualifiedNameString(referenceDeclaration), referenceKind, | 97 | var referenceInfo = new RelationInfo(getQualifiedNameString(referenceDeclaration), referenceRole, |
95 | List.of(sourceParameter, targetParameter), multiplicity, referenceDeclaration.getOpposite(), | 98 | List.of(sourceParameter, targetParameter), multiplicity, referenceDeclaration.getOpposite(), |
96 | List.of()); | 99 | List.of()); |
97 | this.relations.put(referenceDeclaration, referenceInfo); | 100 | this.relations.put(referenceDeclaration, referenceInfo); |
@@ -101,7 +104,7 @@ class SymbolCollector { | |||
101 | private void collectEnum(EnumDeclaration enumDeclaration) { | 104 | private void collectEnum(EnumDeclaration enumDeclaration) { |
102 | var instanceParameter = ProblemFactory.eINSTANCE.createParameter(); | 105 | var instanceParameter = ProblemFactory.eINSTANCE.createParameter(); |
103 | instanceParameter.setName("instance"); | 106 | instanceParameter.setName("instance"); |
104 | var info = new RelationInfo(getQualifiedNameString(enumDeclaration), PredicateKind.DEFAULT, | 107 | var info = new RelationInfo(getQualifiedNameString(enumDeclaration), ContainmentRole.NONE, |
105 | List.of(instanceParameter), null, null, List.of()); | 108 | List.of(instanceParameter), null, null, List.of()); |
106 | this.relations.put(enumDeclaration, info); | 109 | this.relations.put(enumDeclaration, info); |
107 | } | 110 | } |
@@ -172,6 +175,8 @@ class SymbolCollector { | |||
172 | collectAssertion(assertion); | 175 | collectAssertion(assertion); |
173 | } else if (statement instanceof NodeValueAssertion nodeValueAssertion) { | 176 | } else if (statement instanceof NodeValueAssertion nodeValueAssertion) { |
174 | collectNodeValueAssertion(nodeValueAssertion); | 177 | collectNodeValueAssertion(nodeValueAssertion); |
178 | } else if (statement instanceof PredicateDefinition predicateDefinition) { | ||
179 | collectPredicateAssertion(predicateDefinition); | ||
175 | } else if (statement instanceof ClassDeclaration classDeclaration) { | 180 | } else if (statement instanceof ClassDeclaration classDeclaration) { |
176 | collectClassAssertion(classDeclaration); | 181 | collectClassAssertion(classDeclaration); |
177 | } else if (statement instanceof EnumDeclaration enumDeclaration) { | 182 | } else if (statement instanceof EnumDeclaration enumDeclaration) { |
@@ -190,11 +195,7 @@ class SymbolCollector { | |||
190 | // Problem during editing. The errors can still be detected by the Problem validator. | 195 | // Problem during editing. The errors can still be detected by the Problem validator. |
191 | return; | 196 | return; |
192 | } | 197 | } |
193 | if (assertion.isDefault()) { | 198 | relationInfo.assertions().add(assertion); |
194 | relationInfo.defaultAssertions().add(assertion); | ||
195 | } else { | ||
196 | relationInfo.assertions().add(assertion); | ||
197 | } | ||
198 | for (var argument : assertion.getArguments()) { | 199 | for (var argument : assertion.getArguments()) { |
199 | if (argument instanceof ConstantAssertionArgument constantAssertionArgument) { | 200 | if (argument instanceof ConstantAssertionArgument constantAssertionArgument) { |
200 | var constantNode = constantAssertionArgument.getNode(); | 201 | var constantNode = constantAssertionArgument.getNode(); |
@@ -239,6 +240,14 @@ class SymbolCollector { | |||
239 | addAssertion(dataType, LogicValue.TRUE, node); | 240 | addAssertion(dataType, LogicValue.TRUE, node); |
240 | } | 241 | } |
241 | 242 | ||
243 | private void collectPredicateAssertion(PredicateDefinition predicateDefinition) { | ||
244 | if (predicateDefinition.getKind() != PredicateKind.ERROR) { | ||
245 | return; | ||
246 | } | ||
247 | int arity = predicateDefinition.getParameters().size(); | ||
248 | addAssertion(predicateDefinition, LogicValue.FALSE, new Node[arity]); | ||
249 | } | ||
250 | |||
242 | private void collectClassAssertion(ClassDeclaration classDeclaration) { | 251 | private void collectClassAssertion(ClassDeclaration classDeclaration) { |
243 | var node = classDeclaration.getNewNode(); | 252 | var node = classDeclaration.getNewNode(); |
244 | if (node == null) { | 253 | if (node == null) { |
@@ -259,8 +268,14 @@ class SymbolCollector { | |||
259 | var assertion = ProblemFactory.eINSTANCE.createAssertion(); | 268 | var assertion = ProblemFactory.eINSTANCE.createAssertion(); |
260 | assertion.setRelation(relation); | 269 | assertion.setRelation(relation); |
261 | for (var node : nodes) { | 270 | for (var node : nodes) { |
262 | var argument = ProblemFactory.eINSTANCE.createNodeAssertionArgument(); | 271 | AssertionArgument argument; |
263 | argument.setNode(node); | 272 | if (node == null) { |
273 | argument = ProblemFactory.eINSTANCE.createWildcardAssertionArgument(); | ||
274 | } else { | ||
275 | var nodeArgument = ProblemFactory.eINSTANCE.createNodeAssertionArgument(); | ||
276 | nodeArgument.setNode(node); | ||
277 | argument = nodeArgument; | ||
278 | } | ||
264 | assertion.getArguments().add(argument); | 279 | assertion.getArguments().add(argument); |
265 | } | 280 | } |
266 | assertion.setValue(logicValue); | 281 | assertion.setValue(logicValue); |