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-semantics/src | |
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-semantics/src')
-rw-r--r-- | subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java | 91 |
1 files changed, 89 insertions, 2 deletions
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 830d4a2c..0378983c 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 | |||
@@ -1,9 +1,96 @@ | |||
1 | package tools.refinery.language.semantics.model; | 1 | package tools.refinery.language.semantics.model; |
2 | 2 | ||
3 | import tools.refinery.language.utils.CollectedSymbols; | 3 | import com.google.inject.Inject; |
4 | import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; | ||
5 | import org.eclipse.collections.api.map.primitive.MutableObjectIntMap; | ||
6 | import tools.refinery.language.model.problem.*; | ||
7 | import tools.refinery.language.semantics.model.internal.DecisionTree; | ||
8 | import tools.refinery.language.utils.ProblemDesugarer; | ||
9 | import tools.refinery.language.utils.RelationInfo; | ||
10 | import tools.refinery.store.model.representation.Relation; | ||
11 | import tools.refinery.store.model.representation.TruthValue; | ||
12 | import tools.refinery.store.tuple.Tuple; | ||
13 | |||
14 | import java.util.HashMap; | ||
15 | import java.util.Map; | ||
4 | 16 | ||
5 | public class ModelInitializer { | 17 | public class ModelInitializer { |
6 | public void createModel(CollectedSymbols symbols) { | 18 | @Inject |
19 | private ProblemDesugarer desugarer; | ||
20 | |||
21 | private final MutableObjectIntMap<Node> nodeTrace = ObjectIntMaps.mutable.empty(); | ||
22 | |||
23 | private final Map<tools.refinery.language.model.problem.Relation, Relation<TruthValue>> relationTrace = | ||
24 | new HashMap<>(); | ||
25 | |||
26 | private int nodeCount = 0; | ||
27 | |||
28 | public void createModel(Problem problem) { | ||
29 | var builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException( | ||
30 | "Problem has no builtin library")); | ||
31 | var collectedSymbols = desugarer.collectSymbols(problem); | ||
32 | for (var node : collectedSymbols.nodes().keySet()) { | ||
33 | nodeTrace.put(node, nodeCount); | ||
34 | nodeCount += 1; | ||
35 | } | ||
36 | for (var pair : collectedSymbols.relations().entrySet()) { | ||
37 | var relation = pair.getKey(); | ||
38 | var relationInfo = pair.getValue(); | ||
39 | var isEqualsRelation = relation == builtinSymbols.equals(); | ||
40 | var decisionTree = mergeAssertions(relationInfo, isEqualsRelation); | ||
41 | var defaultValue = isEqualsRelation ? TruthValue.FALSE : TruthValue.UNKNOWN; | ||
42 | relationTrace.put(relation, new Relation<>(relationInfo.name(), relationInfo.arity(), defaultValue)); | ||
43 | } | ||
44 | } | ||
45 | |||
46 | private DecisionTree mergeAssertions(RelationInfo relationInfo, boolean isEqualsRelation) { | ||
47 | var arity = relationInfo.arity(); | ||
48 | var defaultAssertions = new DecisionTree(arity, isEqualsRelation ? null : TruthValue.UNKNOWN); | ||
49 | var assertions = new DecisionTree(arity); | ||
50 | for (var assertion : relationInfo.assertions()) { | ||
51 | var tuple = getTuple(assertion); | ||
52 | var value = getTruthValue(assertion.getValue()); | ||
53 | if (assertion.isDefault()) { | ||
54 | defaultAssertions.mergeValue(tuple, value); | ||
55 | } else { | ||
56 | assertions.mergeValue(tuple, value); | ||
57 | } | ||
58 | } | ||
59 | defaultAssertions.overwriteValues(assertions); | ||
60 | if (isEqualsRelation) { | ||
61 | for (int i = 0; i < nodeCount; i++) { | ||
62 | defaultAssertions.setIfMissing(Tuple.of(i, i), TruthValue.TRUE); | ||
63 | } | ||
64 | defaultAssertions.setAllMissing(TruthValue.FALSE); | ||
65 | } | ||
66 | return defaultAssertions; | ||
67 | } | ||
68 | |||
69 | private Tuple getTuple(Assertion assertion) { | ||
70 | var arguments = assertion.getArguments(); | ||
71 | int arity = arguments.size(); | ||
72 | var nodes = new int[arity]; | ||
73 | for (int i = 0; i < arity; i++) { | ||
74 | var argument = arguments.get(i); | ||
75 | if (argument instanceof NodeAssertionArgument nodeArgument) { | ||
76 | nodes[i] = nodeTrace.getOrThrow(nodeArgument.getNode()); | ||
77 | } else if (argument instanceof ConstantAssertionArgument constantArgument) { | ||
78 | nodes[i] = nodeTrace.getOrThrow(constantArgument.getNode()); | ||
79 | } else if (argument instanceof WildcardAssertionArgument) { | ||
80 | nodes[i] = -1; | ||
81 | } else { | ||
82 | throw new IllegalArgumentException("Unknown assertion argument: " + argument); | ||
83 | } | ||
84 | } | ||
85 | return Tuple.of(nodes); | ||
86 | } | ||
7 | 87 | ||
88 | private static TruthValue getTruthValue(LogicValue value) { | ||
89 | return switch (value) { | ||
90 | case TRUE -> TruthValue.TRUE; | ||
91 | case FALSE -> TruthValue.FALSE; | ||
92 | case UNKNOWN -> TruthValue.UNKNOWN; | ||
93 | case ERROR -> TruthValue.ERROR; | ||
94 | }; | ||
8 | } | 95 | } |
9 | } | 96 | } |