diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-09-07 18:04:42 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-09-07 18:04:42 +0200 |
commit | a128e05f18a101983d331d0819008740b521d6df (patch) | |
tree | cc23c330eea900ab7b513a6c21a241ebf0795785 /subprojects/store-reasoning | |
parent | feat(dse): transformation rule builder (diff) | |
download | refinery-a128e05f18a101983d331d0819008740b521d6df.tar.gz refinery-a128e05f18a101983d331d0819008740b521d6df.tar.zst refinery-a128e05f18a101983d331d0819008740b521d6df.zip |
feat: declarative DSE rules and model refinement
Diffstat (limited to 'subprojects/store-reasoning')
17 files changed, 543 insertions, 31 deletions
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java index 17aec09c..1dda7ac1 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java | |||
@@ -42,6 +42,9 @@ public interface ReasoningAdapter extends ModelAdapter { | |||
42 | @Nullable | 42 | @Nullable |
43 | Tuple1 split(int parentMultiObject); | 43 | Tuple1 split(int parentMultiObject); |
44 | 44 | ||
45 | @Nullable | ||
46 | Tuple1 focus(int parentObject); | ||
47 | |||
45 | boolean cleanup(int nodeToDelete); | 48 | boolean cleanup(int nodeToDelete); |
46 | 49 | ||
47 | static ReasoningBuilder builder() { | 50 | static ReasoningBuilder builder() { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java index 3d4c672f..79bce33e 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java | |||
@@ -6,6 +6,7 @@ | |||
6 | package tools.refinery.store.reasoning; | 6 | package tools.refinery.store.reasoning; |
7 | 7 | ||
8 | import tools.refinery.store.adapter.ModelAdapterBuilder; | 8 | import tools.refinery.store.adapter.ModelAdapterBuilder; |
9 | import tools.refinery.store.dse.transition.objectives.Objective; | ||
9 | import tools.refinery.store.model.ModelStore; | 10 | import tools.refinery.store.model.ModelStore; |
10 | import tools.refinery.store.query.dnf.Dnf; | 11 | import tools.refinery.store.query.dnf.Dnf; |
11 | import tools.refinery.store.query.dnf.FunctionalQuery; | 12 | import tools.refinery.store.query.dnf.FunctionalQuery; |
@@ -35,6 +36,17 @@ public interface ReasoningBuilder extends ModelAdapterBuilder { | |||
35 | 36 | ||
36 | ReasoningBuilder initializer(PartialModelInitializer initializer); | 37 | ReasoningBuilder initializer(PartialModelInitializer initializer); |
37 | 38 | ||
39 | ReasoningBuilder objective(Objective objective); | ||
40 | |||
41 | default ReasoningBuilder objectives(Objective... objectives) { | ||
42 | return objectives(List.of(objectives)); | ||
43 | } | ||
44 | |||
45 | default ReasoningBuilder objectives(Collection<Objective> objectives) { | ||
46 | objectives.forEach(this::objective); | ||
47 | return this; | ||
48 | } | ||
49 | |||
38 | <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query); | 50 | <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query); |
39 | 51 | ||
40 | RelationalQuery lift(Modality modality, Concreteness concreteness, RelationalQuery query); | 52 | RelationalQuery lift(Modality modality, Concreteness concreteness, RelationalQuery query); |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/FocusActionLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/FocusActionLiteral.java new file mode 100644 index 00000000..5a6f22d2 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/FocusActionLiteral.java | |||
@@ -0,0 +1,48 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.actions; | ||
7 | |||
8 | import tools.refinery.store.dse.transition.actions.AbstractActionLiteral; | ||
9 | import tools.refinery.store.dse.transition.actions.BoundActionLiteral; | ||
10 | import tools.refinery.store.model.Model; | ||
11 | import tools.refinery.store.query.term.NodeVariable; | ||
12 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
13 | |||
14 | import java.util.List; | ||
15 | |||
16 | public class FocusActionLiteral extends AbstractActionLiteral { | ||
17 | private final NodeVariable parentNode; | ||
18 | private final NodeVariable childNode; | ||
19 | |||
20 | public FocusActionLiteral(NodeVariable parentNode, NodeVariable childNode) { | ||
21 | this.parentNode = parentNode; | ||
22 | this.childNode = childNode; | ||
23 | } | ||
24 | |||
25 | public NodeVariable getParentNode() { | ||
26 | return parentNode; | ||
27 | } | ||
28 | |||
29 | public NodeVariable getChildNode() { | ||
30 | return childNode; | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public List<NodeVariable> getInputVariables() { | ||
35 | return List.of(parentNode); | ||
36 | } | ||
37 | |||
38 | @Override | ||
39 | public List<NodeVariable> getOutputVariables() { | ||
40 | return List.of(childNode); | ||
41 | } | ||
42 | |||
43 | @Override | ||
44 | public BoundActionLiteral bindToModel(Model model) { | ||
45 | var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
46 | return tuple -> reasoningAdapter.focus(tuple.get(0)); | ||
47 | } | ||
48 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/MergeActionLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/MergeActionLiteral.java new file mode 100644 index 00000000..8d0d7961 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/MergeActionLiteral.java | |||
@@ -0,0 +1,60 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.actions; | ||
7 | |||
8 | import tools.refinery.store.dse.transition.actions.AbstractActionLiteral; | ||
9 | import tools.refinery.store.dse.transition.actions.BoundActionLiteral; | ||
10 | import tools.refinery.store.model.Model; | ||
11 | import tools.refinery.store.query.term.NodeVariable; | ||
12 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
13 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
14 | import tools.refinery.store.tuple.Tuple; | ||
15 | |||
16 | import java.util.List; | ||
17 | |||
18 | public class MergeActionLiteral<A, C> extends AbstractActionLiteral { | ||
19 | private final PartialSymbol<A, C> partialSymbol; | ||
20 | private final List<NodeVariable> parameters; | ||
21 | private final A value; | ||
22 | |||
23 | public MergeActionLiteral(PartialSymbol<A, C> partialSymbol, A value, List<NodeVariable> parameters) { | ||
24 | if (partialSymbol.arity() != parameters.size()) { | ||
25 | throw new IllegalArgumentException("Expected %d parameters for partial symbol %s, got %d instead" | ||
26 | .formatted(partialSymbol.arity(), partialSymbol, parameters.size())); | ||
27 | } | ||
28 | this.partialSymbol = partialSymbol; | ||
29 | this.parameters = parameters; | ||
30 | this.value = value; | ||
31 | } | ||
32 | |||
33 | public PartialSymbol<A, C> getPartialSymbol() { | ||
34 | return partialSymbol; | ||
35 | } | ||
36 | |||
37 | public List<NodeVariable> getParameters() { | ||
38 | return parameters; | ||
39 | } | ||
40 | |||
41 | public A getValue() { | ||
42 | return value; | ||
43 | } | ||
44 | |||
45 | @Override | ||
46 | public List<NodeVariable> getInputVariables() { | ||
47 | return getParameters(); | ||
48 | } | ||
49 | |||
50 | @Override | ||
51 | public List<NodeVariable> getOutputVariables() { | ||
52 | return List.of(); | ||
53 | } | ||
54 | |||
55 | @Override | ||
56 | public BoundActionLiteral bindToModel(Model model) { | ||
57 | var refiner = model.getAdapter(ReasoningAdapter.class).getRefiner(partialSymbol); | ||
58 | return tuple -> refiner.merge(tuple, value) ? Tuple.of() : null; | ||
59 | } | ||
60 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java new file mode 100644 index 00000000..990d11e5 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java | |||
@@ -0,0 +1,38 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.actions; | ||
7 | |||
8 | import tools.refinery.store.query.term.NodeVariable; | ||
9 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
10 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
11 | import tools.refinery.store.representation.TruthValue; | ||
12 | |||
13 | import java.util.List; | ||
14 | |||
15 | public final class PartialActionLiterals { | ||
16 | private PartialActionLiterals() { | ||
17 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); | ||
18 | } | ||
19 | |||
20 | public static <A, C> MergeActionLiteral<A, C> merge(PartialSymbol<A, C> partialSymbol, A value, | ||
21 | NodeVariable... parameters) { | ||
22 | return new MergeActionLiteral<>(partialSymbol, value, List.of(parameters)); | ||
23 | } | ||
24 | |||
25 | public static MergeActionLiteral<TruthValue, Boolean> add(PartialRelation partialRelation, | ||
26 | NodeVariable... parameters) { | ||
27 | return merge(partialRelation, TruthValue.TRUE, parameters); | ||
28 | } | ||
29 | |||
30 | public static MergeActionLiteral<TruthValue, Boolean> remove(PartialRelation partialRelation, | ||
31 | NodeVariable... parameters) { | ||
32 | return merge(partialRelation, TruthValue.FALSE, parameters); | ||
33 | } | ||
34 | |||
35 | public static FocusActionLiteral focus(NodeVariable parent, NodeVariable child) { | ||
36 | return new FocusActionLiteral(parent, child); | ||
37 | } | ||
38 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java index 2fa744de..f91fdd07 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java | |||
@@ -17,7 +17,10 @@ import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | |||
17 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | 17 | import tools.refinery.store.reasoning.refinement.StorageRefiner; |
18 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 18 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
19 | import tools.refinery.store.reasoning.representation.PartialSymbol; | 19 | import tools.refinery.store.reasoning.representation.PartialSymbol; |
20 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
20 | import tools.refinery.store.representation.Symbol; | 21 | import tools.refinery.store.representation.Symbol; |
22 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
23 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
21 | import tools.refinery.store.tuple.Tuple; | 24 | import tools.refinery.store.tuple.Tuple; |
22 | import tools.refinery.store.tuple.Tuple1; | 25 | import tools.refinery.store.tuple.Tuple1; |
23 | 26 | ||
@@ -32,6 +35,7 @@ class ReasoningAdapterImpl implements ReasoningAdapter { | |||
32 | private final Map<AnyPartialSymbol, AnyPartialInterpretationRefiner> refiners; | 35 | private final Map<AnyPartialSymbol, AnyPartialInterpretationRefiner> refiners; |
33 | private final StorageRefiner[] storageRefiners; | 36 | private final StorageRefiner[] storageRefiners; |
34 | private final Interpretation<Integer> nodeCountInterpretation; | 37 | private final Interpretation<Integer> nodeCountInterpretation; |
38 | private final Interpretation<CardinalityInterval> countInterpretation; | ||
35 | 39 | ||
36 | ReasoningAdapterImpl(Model model, ReasoningStoreAdapterImpl storeAdapter) { | 40 | ReasoningAdapterImpl(Model model, ReasoningStoreAdapterImpl storeAdapter) { |
37 | this.model = model; | 41 | this.model = model; |
@@ -51,6 +55,11 @@ class ReasoningAdapterImpl implements ReasoningAdapter { | |||
51 | storageRefiners = storeAdapter.createStorageRefiner(model); | 55 | storageRefiners = storeAdapter.createStorageRefiner(model); |
52 | 56 | ||
53 | nodeCountInterpretation = model.getInterpretation(NODE_COUNT_SYMBOL); | 57 | nodeCountInterpretation = model.getInterpretation(NODE_COUNT_SYMBOL); |
58 | if (model.getStore().getSymbols().contains(MultiObjectTranslator.COUNT_STORAGE)) { | ||
59 | countInterpretation = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE); | ||
60 | } else { | ||
61 | countInterpretation = null; | ||
62 | } | ||
54 | } | 63 | } |
55 | 64 | ||
56 | private void createPartialInterpretations() { | 65 | private void createPartialInterpretations() { |
@@ -161,6 +170,26 @@ class ReasoningAdapterImpl implements ReasoningAdapter { | |||
161 | } | 170 | } |
162 | 171 | ||
163 | @Override | 172 | @Override |
173 | public @Nullable Tuple1 focus(int parentObject) { | ||
174 | if (countInterpretation == null) { | ||
175 | throw new IllegalStateException("Cannot focus without " + MultiObjectTranslator.class.getSimpleName()); | ||
176 | } | ||
177 | var tuple = Tuple.of(parentObject); | ||
178 | var count = countInterpretation.get(tuple); | ||
179 | if (CardinalityIntervals.ONE.equals(count)) { | ||
180 | return tuple; | ||
181 | } | ||
182 | if (CardinalityIntervals.LONE.equals(count)) { | ||
183 | countInterpretation.put(tuple, CardinalityIntervals.ONE); | ||
184 | return tuple; | ||
185 | } | ||
186 | if (CardinalityIntervals.NONE.equals(count)) { | ||
187 | return null; | ||
188 | } | ||
189 | return split(parentObject); | ||
190 | } | ||
191 | |||
192 | @Override | ||
164 | public boolean cleanup(int nodeToDelete) { | 193 | public boolean cleanup(int nodeToDelete) { |
165 | // Avoid creating an iterator object. | 194 | // Avoid creating an iterator object. |
166 | //noinspection ForLoopReplaceableByForEach | 195 | //noinspection ForLoopReplaceableByForEach |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java index b4971d2c..d2cd2eb0 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java | |||
@@ -6,6 +6,9 @@ | |||
6 | package tools.refinery.store.reasoning.internal; | 6 | package tools.refinery.store.reasoning.internal; |
7 | 7 | ||
8 | import tools.refinery.store.adapter.AbstractModelAdapterBuilder; | 8 | import tools.refinery.store.adapter.AbstractModelAdapterBuilder; |
9 | import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; | ||
10 | import tools.refinery.store.dse.transition.objectives.Objective; | ||
11 | import tools.refinery.store.dse.transition.objectives.Objectives; | ||
9 | import tools.refinery.store.model.ModelStore; | 12 | import tools.refinery.store.model.ModelStore; |
10 | import tools.refinery.store.model.ModelStoreBuilder; | 13 | import tools.refinery.store.model.ModelStoreBuilder; |
11 | import tools.refinery.store.query.ModelQueryBuilder; | 14 | import tools.refinery.store.query.ModelQueryBuilder; |
@@ -36,11 +39,13 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningS | |||
36 | private final PartialQueryRewriter queryRewriter = new PartialQueryRewriter(lifter); | 39 | private final PartialQueryRewriter queryRewriter = new PartialQueryRewriter(lifter); |
37 | private Set<Concreteness> requiredInterpretations = Set.of(Concreteness.values()); | 40 | private Set<Concreteness> requiredInterpretations = Set.of(Concreteness.values()); |
38 | private final Map<AnyPartialSymbol, AnyPartialSymbolTranslator> translators = new LinkedHashMap<>(); | 41 | private final Map<AnyPartialSymbol, AnyPartialSymbolTranslator> translators = new LinkedHashMap<>(); |
39 | private final Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters = new LinkedHashMap<>(); | 42 | private final Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters = |
43 | new LinkedHashMap<>(); | ||
40 | private final Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners = | 44 | private final Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners = |
41 | new LinkedHashMap<>(); | 45 | new LinkedHashMap<>(); |
42 | private final Map<AnySymbol, StorageRefiner.Factory<?>> registeredStorageRefiners = new LinkedHashMap<>(); | 46 | private final Map<AnySymbol, StorageRefiner.Factory<?>> registeredStorageRefiners = new LinkedHashMap<>(); |
43 | private final List<PartialModelInitializer> initializers = new ArrayList<>(); | 47 | private final List<PartialModelInitializer> initializers = new ArrayList<>(); |
48 | private final List<Objective> objectives = new ArrayList<>(); | ||
44 | 49 | ||
45 | @Override | 50 | @Override |
46 | public ReasoningBuilder requiredInterpretations(Collection<Concreteness> requiredInterpretations) { | 51 | public ReasoningBuilder requiredInterpretations(Collection<Concreteness> requiredInterpretations) { |
@@ -75,6 +80,13 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningS | |||
75 | } | 80 | } |
76 | 81 | ||
77 | @Override | 82 | @Override |
83 | public ReasoningBuilder objective(Objective objective) { | ||
84 | checkNotConfigured(); | ||
85 | objectives.add(objective); | ||
86 | return this; | ||
87 | } | ||
88 | |||
89 | @Override | ||
78 | public <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query) { | 90 | public <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query) { |
79 | return lifter.lift(modality, concreteness, query); | 91 | return lifter.lift(modality, concreteness, query); |
80 | } | 92 | } |
@@ -109,6 +121,10 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningS | |||
109 | storeBuilder.symbols(registeredStorageRefiners.keySet()); | 121 | storeBuilder.symbols(registeredStorageRefiners.keySet()); |
110 | var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class); | 122 | var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class); |
111 | queryBuilder.rewriter(queryRewriter); | 123 | queryBuilder.rewriter(queryRewriter); |
124 | if (!objectives.isEmpty()) { | ||
125 | storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class) | ||
126 | .ifPresent(dseBuilder -> dseBuilder.objective(Objectives.sum(objectives))); | ||
127 | } | ||
112 | } | 128 | } |
113 | 129 | ||
114 | private void doConfigure(ModelStoreBuilder storeBuilder, PartialRelationTranslator relationConfiguration) { | 130 | private void doConfigure(ModelStoreBuilder storeBuilder, PartialRelationTranslator relationConfiguration) { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java index 4600d5a4..c2039afc 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java | |||
@@ -5,14 +5,21 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator; | 6 | package tools.refinery.store.reasoning.translator; |
7 | 7 | ||
8 | import tools.refinery.store.dse.transition.Rule; | ||
9 | import tools.refinery.store.dse.transition.objectives.Criteria; | ||
10 | import tools.refinery.store.dse.transition.objectives.Criterion; | ||
11 | import tools.refinery.store.dse.transition.objectives.Objective; | ||
12 | import tools.refinery.store.dse.transition.objectives.Objectives; | ||
8 | import tools.refinery.store.model.ModelStoreBuilder; | 13 | import tools.refinery.store.model.ModelStoreBuilder; |
9 | import tools.refinery.store.query.Constraint; | 14 | import tools.refinery.store.query.Constraint; |
10 | import tools.refinery.store.query.dnf.Query; | 15 | import tools.refinery.store.query.dnf.Query; |
11 | import tools.refinery.store.query.dnf.QueryBuilder; | 16 | import tools.refinery.store.query.dnf.QueryBuilder; |
12 | import tools.refinery.store.query.dnf.RelationalQuery; | 17 | import tools.refinery.store.query.dnf.RelationalQuery; |
13 | import tools.refinery.store.query.term.Variable; | 18 | import tools.refinery.store.query.literal.Literal; |
19 | import tools.refinery.store.query.term.NodeVariable; | ||
14 | import tools.refinery.store.query.view.MayView; | 20 | import tools.refinery.store.query.view.MayView; |
15 | import tools.refinery.store.query.view.MustView; | 21 | import tools.refinery.store.query.view.MustView; |
22 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
16 | import tools.refinery.store.reasoning.ReasoningBuilder; | 23 | import tools.refinery.store.reasoning.ReasoningBuilder; |
17 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | 24 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; |
18 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; | 25 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; |
@@ -21,6 +28,7 @@ import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter; | |||
21 | import tools.refinery.store.reasoning.lifting.DnfLifter; | 28 | import tools.refinery.store.reasoning.lifting.DnfLifter; |
22 | import tools.refinery.store.reasoning.literal.Concreteness; | 29 | import tools.refinery.store.reasoning.literal.Concreteness; |
23 | import tools.refinery.store.reasoning.literal.Modality; | 30 | import tools.refinery.store.reasoning.literal.Modality; |
31 | import tools.refinery.store.reasoning.literal.PartialLiterals; | ||
24 | import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner; | 32 | import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner; |
25 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | 33 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; |
26 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | 34 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; |
@@ -30,8 +38,11 @@ import tools.refinery.store.representation.AnySymbol; | |||
30 | import tools.refinery.store.representation.Symbol; | 38 | import tools.refinery.store.representation.Symbol; |
31 | import tools.refinery.store.representation.TruthValue; | 39 | import tools.refinery.store.representation.TruthValue; |
32 | 40 | ||
41 | import java.util.ArrayList; | ||
33 | import java.util.function.BiConsumer; | 42 | import java.util.function.BiConsumer; |
34 | 43 | ||
44 | import static tools.refinery.store.query.literal.Literals.not; | ||
45 | |||
35 | @SuppressWarnings("UnusedReturnValue") | 46 | @SuppressWarnings("UnusedReturnValue") |
36 | public final class PartialRelationTranslator extends PartialSymbolTranslator<TruthValue, Boolean> { | 47 | public final class PartialRelationTranslator extends PartialSymbolTranslator<TruthValue, Boolean> { |
37 | private final PartialRelation partialRelation; | 48 | private final PartialRelation partialRelation; |
@@ -94,6 +105,30 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
94 | return this; | 105 | return this; |
95 | } | 106 | } |
96 | 107 | ||
108 | @Override | ||
109 | public PartialRelationTranslator decision(Rule decisionRule) { | ||
110 | super.decision(decisionRule); | ||
111 | return this; | ||
112 | } | ||
113 | |||
114 | @Override | ||
115 | public PartialRelationTranslator accept(Criterion acceptanceCriterion) { | ||
116 | super.accept(acceptanceCriterion); | ||
117 | return this; | ||
118 | } | ||
119 | |||
120 | @Override | ||
121 | public PartialRelationTranslator exclude(Criterion exclusionCriterion) { | ||
122 | super.exclude(exclusionCriterion); | ||
123 | return this; | ||
124 | } | ||
125 | |||
126 | @Override | ||
127 | public PartialRelationTranslator objective(Objective objective) { | ||
128 | super.objective(objective); | ||
129 | return this; | ||
130 | } | ||
131 | |||
97 | public PartialRelationTranslator query(RelationalQuery query) { | 132 | public PartialRelationTranslator query(RelationalQuery query) { |
98 | checkNotConfigured(); | 133 | checkNotConfigured(); |
99 | if (this.query != null) { | 134 | if (this.query != null) { |
@@ -170,6 +205,8 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
170 | createFallbackRewriter(); | 205 | createFallbackRewriter(); |
171 | createFallbackInterpretation(); | 206 | createFallbackInterpretation(); |
172 | createFallbackRefiner(); | 207 | createFallbackRefiner(); |
208 | createFallbackExclude(); | ||
209 | createFallbackObjective(); | ||
173 | super.doConfigure(storeBuilder); | 210 | super.doConfigure(storeBuilder); |
174 | } | 211 | } |
175 | 212 | ||
@@ -179,10 +216,10 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
179 | } | 216 | } |
180 | } | 217 | } |
181 | 218 | ||
182 | private RelationalQuery createQuery(String name, BiConsumer<QueryBuilder, Variable[]> callback) { | 219 | private RelationalQuery createQuery(String name, BiConsumer<QueryBuilder, NodeVariable[]> callback) { |
183 | int arity = partialRelation.arity(); | 220 | int arity = partialRelation.arity(); |
184 | var queryBuilder = Query.builder(name); | 221 | var queryBuilder = Query.builder(name); |
185 | var parameters = new Variable[arity]; | 222 | var parameters = new NodeVariable[arity]; |
186 | for (int i = 0; i < arity; i++) { | 223 | for (int i = 0; i < arity; i++) { |
187 | parameters[i] = queryBuilder.parameter("p" + 1); | 224 | parameters[i] = queryBuilder.parameter("p" + 1); |
188 | } | 225 | } |
@@ -293,6 +330,55 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
293 | } | 330 | } |
294 | } | 331 | } |
295 | 332 | ||
333 | private void createFallbackExclude() { | ||
334 | if (excludeWasSet) { | ||
335 | return; | ||
336 | } | ||
337 | var excludeQuery = createQuery("exclude", (builder, parameters) -> { | ||
338 | var literals = new ArrayList<Literal>(parameters.length + 2); | ||
339 | literals.add(PartialLiterals.must(partialRelation.call(parameters))); | ||
340 | literals.add(not(PartialLiterals.may(partialRelation.call(parameters)))); | ||
341 | for (var parameter : parameters) { | ||
342 | literals.add(PartialLiterals.must(ReasoningAdapter.EXISTS_SYMBOL.call(parameter))); | ||
343 | } | ||
344 | builder.clause(literals); | ||
345 | }); | ||
346 | exclude = Criteria.whenHasMatch(excludeQuery); | ||
347 | } | ||
348 | |||
349 | private void createFallbackObjective() { | ||
350 | if (acceptWasSet && objectiveWasSet) { | ||
351 | return; | ||
352 | } | ||
353 | var invalidCandidate = createQuery("invalidCandidate", (builder, parameters) -> builder | ||
354 | .clause( | ||
355 | PartialLiterals.candidateMust(partialRelation.call(parameters)), | ||
356 | not(PartialLiterals.candidateMay(partialRelation.call(parameters))) | ||
357 | ) | ||
358 | .clause( | ||
359 | PartialLiterals.candidateMust(partialRelation.call(parameters)), | ||
360 | not(PartialLiterals.may(partialRelation.call(parameters))) | ||
361 | ) | ||
362 | .clause( | ||
363 | PartialLiterals.must(partialRelation.call(parameters)), | ||
364 | not(PartialLiterals.candidateMay(partialRelation.call(parameters))) | ||
365 | )); | ||
366 | var reject = createQuery("reject", (builder, parameters) -> { | ||
367 | var literals = new ArrayList<Literal>(parameters.length + 1); | ||
368 | literals.add(invalidCandidate.call(parameters)); | ||
369 | for (var parameter : parameters) { | ||
370 | literals.add(PartialLiterals.candidateMust(ReasoningAdapter.EXISTS_SYMBOL.call(parameter))); | ||
371 | } | ||
372 | builder.clause(literals); | ||
373 | }); | ||
374 | if (!acceptWasSet) { | ||
375 | accept = Criteria.whenNoMatch(reject); | ||
376 | } | ||
377 | if (!objectiveWasSet) { | ||
378 | objective = Objectives.count(reject); | ||
379 | } | ||
380 | } | ||
381 | |||
296 | public PartialRelationRewriter getRewriter() { | 382 | public PartialRelationRewriter getRewriter() { |
297 | checkConfigured(); | 383 | checkConfigured(); |
298 | return rewriter; | 384 | return rewriter; |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java index e7e26cb2..6cdb287d 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java | |||
@@ -5,10 +5,14 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator; | 6 | package tools.refinery.store.reasoning.translator; |
7 | 7 | ||
8 | import org.jetbrains.annotations.Nullable; | ||
9 | import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; | ||
10 | import tools.refinery.store.dse.transition.Rule; | ||
11 | import tools.refinery.store.dse.transition.objectives.Criterion; | ||
12 | import tools.refinery.store.dse.transition.objectives.Objective; | ||
8 | import tools.refinery.store.model.ModelStoreBuilder; | 13 | import tools.refinery.store.model.ModelStoreBuilder; |
9 | import tools.refinery.store.reasoning.ReasoningBuilder; | 14 | import tools.refinery.store.reasoning.ReasoningBuilder; |
10 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | 15 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; |
11 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
12 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | 16 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; |
13 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | 17 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; |
14 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | 18 | import tools.refinery.store.reasoning.refinement.StorageRefiner; |
@@ -17,7 +21,8 @@ import tools.refinery.store.reasoning.seed.SeedInitializer; | |||
17 | import tools.refinery.store.representation.AnySymbol; | 21 | import tools.refinery.store.representation.AnySymbol; |
18 | import tools.refinery.store.representation.Symbol; | 22 | import tools.refinery.store.representation.Symbol; |
19 | 23 | ||
20 | import java.util.Set; | 24 | import java.util.ArrayList; |
25 | import java.util.List; | ||
21 | 26 | ||
22 | @SuppressWarnings("UnusedReturnValue") | 27 | @SuppressWarnings("UnusedReturnValue") |
23 | public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartialSymbolTranslator | 28 | public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartialSymbolTranslator |
@@ -29,6 +34,13 @@ public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartial | |||
29 | protected StorageRefiner.Factory<?> storageRefiner; | 34 | protected StorageRefiner.Factory<?> storageRefiner; |
30 | protected PartialInterpretation.Factory<A, C> interpretationFactory; | 35 | protected PartialInterpretation.Factory<A, C> interpretationFactory; |
31 | protected PartialModelInitializer initializer; | 36 | protected PartialModelInitializer initializer; |
37 | protected List<Rule> decisionRules = new ArrayList<>(); | ||
38 | protected boolean acceptWasSet; | ||
39 | protected @Nullable Criterion accept; | ||
40 | protected boolean excludeWasSet; | ||
41 | protected @Nullable Criterion exclude; | ||
42 | protected boolean objectiveWasSet; | ||
43 | protected @Nullable Objective objective; | ||
32 | 44 | ||
33 | PartialSymbolTranslator(PartialSymbol<A, C> partialSymbol) { | 45 | PartialSymbolTranslator(PartialSymbol<A, C> partialSymbol) { |
34 | this.partialSymbol = partialSymbol; | 46 | this.partialSymbol = partialSymbol; |
@@ -102,6 +114,38 @@ public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartial | |||
102 | return this; | 114 | return this; |
103 | } | 115 | } |
104 | 116 | ||
117 | public PartialSymbolTranslator<A, C> decision(Rule decisionRule) { | ||
118 | decisionRules.add(decisionRule); | ||
119 | return this; | ||
120 | } | ||
121 | |||
122 | public PartialSymbolTranslator<A, C> accept(@Nullable Criterion acceptanceCriterion) { | ||
123 | if (acceptWasSet) { | ||
124 | throw new IllegalStateException("Accept was already set"); | ||
125 | } | ||
126 | this.accept = acceptanceCriterion; | ||
127 | acceptWasSet = true; | ||
128 | return this; | ||
129 | } | ||
130 | |||
131 | public PartialSymbolTranslator<A, C> exclude(@Nullable Criterion exclusionCriterion) { | ||
132 | if (excludeWasSet) { | ||
133 | throw new IllegalStateException("Exclude was already set"); | ||
134 | } | ||
135 | this.exclude = exclusionCriterion; | ||
136 | excludeWasSet = true; | ||
137 | return this; | ||
138 | } | ||
139 | |||
140 | public PartialSymbolTranslator<A, C> objective(Objective objective) { | ||
141 | if (objectiveWasSet) { | ||
142 | throw new IllegalStateException("Objective was already set"); | ||
143 | } | ||
144 | this.objective = objective; | ||
145 | objectiveWasSet = true; | ||
146 | return this; | ||
147 | } | ||
148 | |||
105 | @Override | 149 | @Override |
106 | public void configure(ModelStoreBuilder storeBuilder) { | 150 | public void configure(ModelStoreBuilder storeBuilder) { |
107 | checkNotConfigured(); | 151 | checkNotConfigured(); |
@@ -124,6 +168,18 @@ public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartial | |||
124 | if (initializer != null) { | 168 | if (initializer != null) { |
125 | reasoningBuilder.initializer(initializer); | 169 | reasoningBuilder.initializer(initializer); |
126 | } | 170 | } |
171 | storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> { | ||
172 | dseBuilder.transformations(decisionRules); | ||
173 | if (accept != null) { | ||
174 | dseBuilder.accept(accept); | ||
175 | } | ||
176 | if (exclude != null) { | ||
177 | dseBuilder.exclude(exclude); | ||
178 | } | ||
179 | }); | ||
180 | if (objective != null) { | ||
181 | reasoningBuilder.objective(objective); | ||
182 | } | ||
127 | } | 183 | } |
128 | 184 | ||
129 | private <T> void registerStorageRefiner(ReasoningBuilder reasoningBuilder, StorageRefiner.Factory<T> factory) { | 185 | private <T> void registerStorageRefiner(ReasoningBuilder reasoningBuilder, StorageRefiner.Factory<T> factory) { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java index dda9f2c8..5c3298ac 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java | |||
@@ -5,6 +5,8 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.containment; | 6 | package tools.refinery.store.reasoning.translator.containment; |
7 | 7 | ||
8 | import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; | ||
9 | import tools.refinery.store.dse.transition.Rule; | ||
8 | import tools.refinery.store.model.ModelStoreBuilder; | 10 | import tools.refinery.store.model.ModelStoreBuilder; |
9 | import tools.refinery.store.model.ModelStoreConfiguration; | 11 | import tools.refinery.store.model.ModelStoreConfiguration; |
10 | import tools.refinery.store.query.dnf.Query; | 12 | import tools.refinery.store.query.dnf.Query; |
@@ -22,6 +24,7 @@ import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer; | |||
22 | import tools.refinery.store.reasoning.representation.PartialRelation; | 24 | import tools.refinery.store.reasoning.representation.PartialRelation; |
23 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | 25 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; |
24 | import tools.refinery.store.reasoning.translator.RoundingMode; | 26 | import tools.refinery.store.reasoning.translator.RoundingMode; |
27 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
25 | import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; | 28 | import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; |
26 | import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; | 29 | import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; |
27 | import tools.refinery.store.representation.Symbol; | 30 | import tools.refinery.store.representation.Symbol; |
@@ -37,8 +40,9 @@ import static tools.refinery.store.query.literal.Literals.not; | |||
37 | import static tools.refinery.store.query.term.int_.IntTerms.constant; | 40 | import static tools.refinery.store.query.term.int_.IntTerms.constant; |
38 | import static tools.refinery.store.query.term.int_.IntTerms.less; | 41 | import static tools.refinery.store.query.term.int_.IntTerms.less; |
39 | import static tools.refinery.store.reasoning.ReasoningAdapter.EXISTS_SYMBOL; | 42 | import static tools.refinery.store.reasoning.ReasoningAdapter.EXISTS_SYMBOL; |
40 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | 43 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add; |
41 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | 44 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.focus; |
45 | import static tools.refinery.store.reasoning.literal.PartialLiterals.*; | ||
42 | 46 | ||
43 | public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { | 47 | public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { |
44 | public static final PartialRelation CONTAINED_SYMBOL = new PartialRelation("contained", 1); | 48 | public static final PartialRelation CONTAINED_SYMBOL = new PartialRelation("contained", 1); |
@@ -104,6 +108,7 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { | |||
104 | translateContainmentLinkType(storeBuilder, linkType, info); | 108 | translateContainmentLinkType(storeBuilder, linkType, info); |
105 | translateInvalidMultiplicity(storeBuilder, linkType, info); | 109 | translateInvalidMultiplicity(storeBuilder, linkType, info); |
106 | } | 110 | } |
111 | translateFocusNotContained(storeBuilder); | ||
107 | } | 112 | } |
108 | 113 | ||
109 | private void translateContainmentLinkType(ModelStoreBuilder storeBuilder, PartialRelation linkType, | 114 | private void translateContainmentLinkType(ModelStoreBuilder storeBuilder, PartialRelation linkType, |
@@ -188,7 +193,17 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { | |||
188 | ))) | 193 | ))) |
189 | .roundingMode(RoundingMode.PREFER_FALSE) | 194 | .roundingMode(RoundingMode.PREFER_FALSE) |
190 | .refiner(ContainmentLinkRefiner.of(linkType, containsStorage, info.sourceType(), info.targetType())) | 195 | .refiner(ContainmentLinkRefiner.of(linkType, containsStorage, info.sourceType(), info.targetType())) |
191 | .initializer(new RefinementBasedInitializer<>(linkType))); | 196 | .initializer(new RefinementBasedInitializer<>(linkType)) |
197 | .decision(Rule.of(linkType.name(), (builder, source, target) -> builder | ||
198 | .clause( | ||
199 | may(linkType.call(source, target)), | ||
200 | not(candidateMust(linkType.call(source, target))), | ||
201 | not(MultiObjectTranslator.MULTI_VIEW.call(source)) | ||
202 | ) | ||
203 | .action(focusedTarget -> List.of( | ||
204 | focus(target, focusedTarget), | ||
205 | add(linkType, source, focusedTarget) | ||
206 | ))))); | ||
192 | } | 207 | } |
193 | 208 | ||
194 | private void translateInvalidMultiplicity(ModelStoreBuilder storeBuilder, PartialRelation linkType, | 209 | private void translateInvalidMultiplicity(ModelStoreBuilder storeBuilder, PartialRelation linkType, |
@@ -216,4 +231,25 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { | |||
216 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(CONTAINED_SYMBOL, CONTAINS_SYMBOL, true, | 231 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(CONTAINED_SYMBOL, CONTAINS_SYMBOL, true, |
217 | ConstrainedMultiplicity.of(CardinalityIntervals.ONE, INVALID_CONTAINER))); | 232 | ConstrainedMultiplicity.of(CardinalityIntervals.ONE, INVALID_CONTAINER))); |
218 | } | 233 | } |
234 | |||
235 | private void translateFocusNotContained(ModelStoreBuilder storeBuilder) { | ||
236 | var dseBuilderOption = storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class); | ||
237 | if (dseBuilderOption.isEmpty()) { | ||
238 | return; | ||
239 | } | ||
240 | var dseBuilder = dseBuilderOption.get(); | ||
241 | dseBuilder.transformation(Rule.of("NOT_CONTAINED", (builder, multi) -> builder | ||
242 | .clause( | ||
243 | MultiObjectTranslator.MULTI_VIEW.call(multi), | ||
244 | not(may(CONTAINED_SYMBOL.call(multi))) | ||
245 | ) | ||
246 | .clause((container) -> List.of( | ||
247 | MultiObjectTranslator.MULTI_VIEW.call(multi), | ||
248 | must(CONTAINS_SYMBOL.call(container, multi)), | ||
249 | not(MultiObjectTranslator.MULTI_VIEW.call(container)) | ||
250 | )) | ||
251 | .action( | ||
252 | focus(multi, Variable.of()) | ||
253 | ))); | ||
254 | } | ||
219 | } | 255 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java index f978aad4..9028337c 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java | |||
@@ -5,6 +5,7 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.crossreference; | 6 | package tools.refinery.store.reasoning.translator.crossreference; |
7 | 7 | ||
8 | import tools.refinery.store.dse.transition.Rule; | ||
8 | import tools.refinery.store.model.ModelStoreBuilder; | 9 | import tools.refinery.store.model.ModelStoreBuilder; |
9 | import tools.refinery.store.model.ModelStoreConfiguration; | 10 | import tools.refinery.store.model.ModelStoreConfiguration; |
10 | import tools.refinery.store.query.dnf.Query; | 11 | import tools.refinery.store.query.dnf.Query; |
@@ -22,8 +23,9 @@ import tools.refinery.store.representation.Symbol; | |||
22 | import tools.refinery.store.representation.TruthValue; | 23 | import tools.refinery.store.representation.TruthValue; |
23 | 24 | ||
24 | import static tools.refinery.store.query.literal.Literals.not; | 25 | import static tools.refinery.store.query.literal.Literals.not; |
25 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | 26 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add; |
26 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | 27 | import static tools.refinery.store.reasoning.literal.PartialLiterals.*; |
28 | import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; | ||
27 | 29 | ||
28 | public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration { | 30 | public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration { |
29 | private final PartialRelation linkType; | 31 | private final PartialRelation linkType; |
@@ -67,7 +69,17 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration | |||
67 | } | 69 | } |
68 | })) | 70 | })) |
69 | .refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType)) | 71 | .refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType)) |
70 | .initializer(new RefinementBasedInitializer<>(linkType))); | 72 | .initializer(new RefinementBasedInitializer<>(linkType)) |
73 | .decision(Rule.of(linkType.name(), (builder, source, target) -> builder | ||
74 | .clause( | ||
75 | may(linkType.call(source, target)), | ||
76 | not(candidateMust(linkType.call(source, target))), | ||
77 | not(MULTI_VIEW.call(source)), | ||
78 | not(MULTI_VIEW.call(target)) | ||
79 | ) | ||
80 | .action( | ||
81 | add(linkType, source, target) | ||
82 | )))); | ||
71 | 83 | ||
72 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(sourceType, linkType, false, | 84 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(sourceType, linkType, false, |
73 | info.sourceMultiplicity())); | 85 | info.sourceMultiplicity())); |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java index e599992d..c554e2a4 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java | |||
@@ -5,6 +5,7 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.crossreference; | 6 | package tools.refinery.store.reasoning.translator.crossreference; |
7 | 7 | ||
8 | import tools.refinery.store.dse.transition.Rule; | ||
8 | import tools.refinery.store.model.ModelStoreBuilder; | 9 | import tools.refinery.store.model.ModelStoreBuilder; |
9 | import tools.refinery.store.model.ModelStoreConfiguration; | 10 | import tools.refinery.store.model.ModelStoreConfiguration; |
10 | import tools.refinery.store.query.dnf.Query; | 11 | import tools.refinery.store.query.dnf.Query; |
@@ -20,8 +21,9 @@ import tools.refinery.store.representation.Symbol; | |||
20 | import tools.refinery.store.representation.TruthValue; | 21 | import tools.refinery.store.representation.TruthValue; |
21 | 22 | ||
22 | import static tools.refinery.store.query.literal.Literals.not; | 23 | import static tools.refinery.store.query.literal.Literals.not; |
23 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | 24 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add; |
24 | import static tools.refinery.store.reasoning.literal.PartialLiterals.must; | 25 | import static tools.refinery.store.reasoning.literal.PartialLiterals.*; |
26 | import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; | ||
25 | 27 | ||
26 | public class UndirectedCrossReferenceTranslator implements ModelStoreConfiguration { | 28 | public class UndirectedCrossReferenceTranslator implements ModelStoreConfiguration { |
27 | private final PartialRelation linkType; | 29 | private final PartialRelation linkType; |
@@ -64,7 +66,17 @@ public class UndirectedCrossReferenceTranslator implements ModelStoreConfigurati | |||
64 | } | 66 | } |
65 | })) | 67 | })) |
66 | .refiner(UndirectedCrossReferenceRefiner.of(symbol, type)) | 68 | .refiner(UndirectedCrossReferenceRefiner.of(symbol, type)) |
67 | .initializer(new RefinementBasedInitializer<>(linkType))); | 69 | .initializer(new RefinementBasedInitializer<>(linkType)) |
70 | .decision(Rule.of(linkType.name(), (builder, source, target) -> builder | ||
71 | .clause( | ||
72 | may(linkType.call(source, target)), | ||
73 | not(candidateMust(linkType.call(source, target))), | ||
74 | not(MULTI_VIEW.call(source)), | ||
75 | not(MULTI_VIEW.call(target)) | ||
76 | ) | ||
77 | .action( | ||
78 | add(linkType, source, target) | ||
79 | )))); | ||
68 | 80 | ||
69 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity())); | 81 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity())); |
70 | } | 82 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java index 735896fa..05704096 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java | |||
@@ -5,9 +5,14 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.multiobject; | 6 | package tools.refinery.store.reasoning.translator.multiobject; |
7 | 7 | ||
8 | import tools.refinery.store.dse.transition.objectives.Criteria; | ||
9 | import tools.refinery.store.dse.transition.objectives.Objectives; | ||
8 | import tools.refinery.store.model.ModelStoreBuilder; | 10 | import tools.refinery.store.model.ModelStoreBuilder; |
9 | import tools.refinery.store.model.ModelStoreConfiguration; | 11 | import tools.refinery.store.model.ModelStoreConfiguration; |
10 | import tools.refinery.store.query.dnf.Query; | 12 | import tools.refinery.store.query.dnf.Query; |
13 | import tools.refinery.store.query.term.Variable; | ||
14 | import tools.refinery.store.query.term.int_.IntTerms; | ||
15 | import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; | ||
11 | import tools.refinery.store.query.view.AnySymbolView; | 16 | import tools.refinery.store.query.view.AnySymbolView; |
12 | import tools.refinery.store.reasoning.ReasoningAdapter; | 17 | import tools.refinery.store.reasoning.ReasoningAdapter; |
13 | import tools.refinery.store.reasoning.ReasoningBuilder; | 18 | import tools.refinery.store.reasoning.ReasoningBuilder; |
@@ -23,16 +28,14 @@ import tools.refinery.store.representation.cardinality.UpperCardinality; | |||
23 | import java.util.List; | 28 | import java.util.List; |
24 | 29 | ||
25 | import static tools.refinery.store.query.literal.Literals.check; | 30 | import static tools.refinery.store.query.literal.Literals.check; |
26 | import static tools.refinery.store.query.term.int_.IntTerms.constant; | 31 | import static tools.refinery.store.query.term.int_.IntTerms.*; |
27 | import static tools.refinery.store.query.term.int_.IntTerms.greaterEq; | ||
28 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.constant; | ||
29 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.greaterEq; | ||
30 | 32 | ||
31 | public class MultiObjectTranslator implements ModelStoreConfiguration { | 33 | public class MultiObjectTranslator implements ModelStoreConfiguration { |
32 | public static final Symbol<CardinalityInterval> COUNT_STORAGE = Symbol.of("COUNT", 1, CardinalityInterval.class, | 34 | public static final Symbol<CardinalityInterval> COUNT_STORAGE = Symbol.of("COUNT", 1, CardinalityInterval.class, |
33 | null); | 35 | null); |
34 | public static final AnySymbolView LOWER_CARDINALITY_VIEW = new LowerCardinalityView(COUNT_STORAGE); | 36 | public static final AnySymbolView LOWER_CARDINALITY_VIEW = new LowerCardinalityView(COUNT_STORAGE); |
35 | public static final AnySymbolView UPPER_CARDINALITY_VIEW = new UpperCardinalityView(COUNT_STORAGE); | 37 | public static final AnySymbolView UPPER_CARDINALITY_VIEW = new UpperCardinalityView(COUNT_STORAGE); |
38 | public static final AnySymbolView MULTI_VIEW = new MultiView(COUNT_STORAGE); | ||
36 | public static final PartialFunction<CardinalityInterval, Integer> COUNT_SYMBOL = new PartialFunction<>("COUNT", 1, | 39 | public static final PartialFunction<CardinalityInterval, Integer> COUNT_SYMBOL = new PartialFunction<>("COUNT", 1, |
37 | CardinalityDomain.INSTANCE); | 40 | CardinalityDomain.INSTANCE); |
38 | 41 | ||
@@ -40,11 +43,23 @@ public class MultiObjectTranslator implements ModelStoreConfiguration { | |||
40 | public void apply(ModelStoreBuilder storeBuilder) { | 43 | public void apply(ModelStoreBuilder storeBuilder) { |
41 | storeBuilder.symbol(COUNT_STORAGE); | 44 | storeBuilder.symbol(COUNT_STORAGE); |
42 | 45 | ||
46 | var aboveLowerBound = Query.of("count#aboveLowerBound", Integer.class, (builder, node, output) -> builder | ||
47 | .clause(Integer.class, lowerBound -> List.of( | ||
48 | LOWER_CARDINALITY_VIEW.call(node, lowerBound), | ||
49 | output.assign(sub(lowerBound, IntTerms.constant(1))), | ||
50 | check(greater(output, IntTerms.constant(0))) | ||
51 | ))); | ||
52 | var missingCardinality = Query.of("count#missing", Integer.class, (builder, output) -> builder | ||
53 | .clause( | ||
54 | output.assign(aboveLowerBound.aggregate(INT_SUM, Variable.of())) | ||
55 | )); | ||
56 | |||
43 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL) | 57 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL) |
44 | .may(Query.of("exists#may", (builder, p1) -> builder | 58 | .may(Query.of("exists#may", (builder, p1) -> builder |
45 | .clause(UpperCardinality.class, upper -> List.of( | 59 | .clause(UpperCardinality.class, upper -> List.of( |
46 | UPPER_CARDINALITY_VIEW.call(p1, upper), | 60 | UPPER_CARDINALITY_VIEW.call(p1, upper), |
47 | check(greaterEq(upper, constant(UpperCardinalities.ONE))) | 61 | check(UpperCardinalityTerms.greaterEq(upper, |
62 | UpperCardinalityTerms.constant(UpperCardinalities.ONE))) | ||
48 | )))) | 63 | )))) |
49 | .must(Query.of("exists#must", (builder, p1) -> builder | 64 | .must(Query.of("exists#must", (builder, p1) -> builder |
50 | .clause(Integer.class, lower -> List.of( | 65 | .clause(Integer.class, lower -> List.of( |
@@ -52,11 +67,17 @@ public class MultiObjectTranslator implements ModelStoreConfiguration { | |||
52 | check(greaterEq(lower, constant(1))) | 67 | check(greaterEq(lower, constant(1))) |
53 | )))) | 68 | )))) |
54 | .roundingMode(RoundingMode.PREFER_FALSE) | 69 | .roundingMode(RoundingMode.PREFER_FALSE) |
55 | .refiner(ExistsRefiner.of(COUNT_STORAGE))); | 70 | .refiner(ExistsRefiner.of(COUNT_STORAGE)) |
71 | .exclude(null) | ||
72 | .accept(Criteria.whenNoMatch(aboveLowerBound)) | ||
73 | .objective(Objectives.value(missingCardinality))); | ||
56 | 74 | ||
57 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EQUALS_SYMBOL) | 75 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EQUALS_SYMBOL) |
58 | .rewriter(EqualsRelationRewriter.of(UPPER_CARDINALITY_VIEW)) | 76 | .rewriter(EqualsRelationRewriter.of(UPPER_CARDINALITY_VIEW)) |
59 | .refiner(EqualsRefiner.of(COUNT_STORAGE))); | 77 | .refiner(EqualsRefiner.of(COUNT_STORAGE)) |
78 | .exclude(null) | ||
79 | .accept(null) | ||
80 | .objective(null)); | ||
60 | 81 | ||
61 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | 82 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); |
62 | reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE)); | 83 | reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE)); |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiView.java new file mode 100644 index 00000000..498bcd83 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiView.java | |||
@@ -0,0 +1,23 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.query.view.TuplePreservingView; | ||
9 | import tools.refinery.store.representation.Symbol; | ||
10 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
11 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
12 | import tools.refinery.store.tuple.Tuple; | ||
13 | |||
14 | class MultiView extends TuplePreservingView<CardinalityInterval> { | ||
15 | protected MultiView(Symbol<CardinalityInterval> symbol) { | ||
16 | super(symbol, "multi"); | ||
17 | } | ||
18 | |||
19 | @Override | ||
20 | protected boolean doFilter(Tuple key, CardinalityInterval value) { | ||
21 | return !CardinalityIntervals.ONE.equals(value); | ||
22 | } | ||
23 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java index c5e5e83e..ee982f4f 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java | |||
@@ -5,6 +5,7 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.multiplicity; | 6 | package tools.refinery.store.reasoning.translator.multiplicity; |
7 | 7 | ||
8 | import tools.refinery.store.dse.transition.objectives.Objectives; | ||
8 | import tools.refinery.store.model.ModelStoreBuilder; | 9 | import tools.refinery.store.model.ModelStoreBuilder; |
9 | import tools.refinery.store.model.ModelStoreConfiguration; | 10 | import tools.refinery.store.model.ModelStoreConfiguration; |
10 | import tools.refinery.store.query.dnf.Query; | 11 | import tools.refinery.store.query.dnf.Query; |
@@ -22,7 +23,10 @@ import tools.refinery.store.representation.cardinality.UpperCardinality; | |||
22 | import java.util.List; | 23 | import java.util.List; |
23 | 24 | ||
24 | import static tools.refinery.store.query.literal.Literals.check; | 25 | import static tools.refinery.store.query.literal.Literals.check; |
26 | import static tools.refinery.store.query.term.int_.IntTerms.INT_SUM; | ||
27 | import static tools.refinery.store.query.term.int_.IntTerms.constant; | ||
25 | import static tools.refinery.store.query.term.int_.IntTerms.greater; | 28 | import static tools.refinery.store.query.term.int_.IntTerms.greater; |
29 | import static tools.refinery.store.query.term.int_.IntTerms.sub; | ||
26 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.constant; | 30 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.constant; |
27 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.less; | 31 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.less; |
28 | import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMust; | 32 | import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMust; |
@@ -67,6 +71,8 @@ public class InvalidMultiplicityErrorTranslator implements ModelStoreConfigurati | |||
67 | .parameter(node); | 71 | .parameter(node); |
68 | var candidateMustBuilder = Query.builder(DnfLifter.decorateName(name, Modality.MUST, Concreteness.PARTIAL)) | 72 | var candidateMustBuilder = Query.builder(DnfLifter.decorateName(name, Modality.MUST, Concreteness.PARTIAL)) |
69 | .parameter(node); | 73 | .parameter(node); |
74 | var missingOutput = Variable.of("missing", Integer.class); | ||
75 | var missingBuilder = Query.builder(name + "#missingMultiplicity").parameter(node).output(missingOutput); | ||
70 | 76 | ||
71 | int lowerBound = cardinalityInterval.lowerBound(); | 77 | int lowerBound = cardinalityInterval.lowerBound(); |
72 | if (lowerBound > 0) { | 78 | if (lowerBound > 0) { |
@@ -79,12 +85,18 @@ public class InvalidMultiplicityErrorTranslator implements ModelStoreConfigurati | |||
79 | candidateMayBuilder.clause(Integer.class, existingContents -> List.of( | 85 | candidateMayBuilder.clause(Integer.class, existingContents -> List.of( |
80 | candidateMust(nodeType.call(node)), | 86 | candidateMust(nodeType.call(node)), |
81 | new CountCandidateLowerBoundLiteral(existingContents, linkType, arguments), | 87 | new CountCandidateLowerBoundLiteral(existingContents, linkType, arguments), |
82 | check(IntTerms.less(existingContents, IntTerms.constant(lowerBound))) | 88 | check(IntTerms.less(existingContents, constant(lowerBound))) |
83 | )); | 89 | )); |
84 | candidateMustBuilder.clause(Integer.class, existingContents -> List.of( | 90 | candidateMustBuilder.clause(Integer.class, existingContents -> List.of( |
85 | candidateMust(nodeType.call(node)), | 91 | candidateMust(nodeType.call(node)), |
86 | new CountCandidateUpperBoundLiteral(existingContents, linkType, arguments), | 92 | new CountCandidateUpperBoundLiteral(existingContents, linkType, arguments), |
87 | check(IntTerms.less(existingContents, IntTerms.constant(lowerBound))) | 93 | check(IntTerms.less(existingContents, constant(lowerBound))) |
94 | )); | ||
95 | missingBuilder.clause(Integer.class, existingContents -> List.of( | ||
96 | candidateMust(nodeType.call(node)), | ||
97 | new CountCandidateLowerBoundLiteral(existingContents, linkType, arguments), | ||
98 | missingOutput.assign(sub(constant(lowerBound), existingContents)), | ||
99 | check(greater(missingOutput, constant(0))) | ||
88 | )); | 100 | )); |
89 | } | 101 | } |
90 | 102 | ||
@@ -93,24 +105,35 @@ public class InvalidMultiplicityErrorTranslator implements ModelStoreConfigurati | |||
93 | mustBuilder.clause(Integer.class, existingContents -> List.of( | 105 | mustBuilder.clause(Integer.class, existingContents -> List.of( |
94 | must(nodeType.call(node)), | 106 | must(nodeType.call(node)), |
95 | new CountLowerBoundLiteral(existingContents, linkType, arguments), | 107 | new CountLowerBoundLiteral(existingContents, linkType, arguments), |
96 | check(greater(existingContents, IntTerms.constant(upperBound))) | 108 | check(greater(existingContents, constant(upperBound))) |
97 | )); | 109 | )); |
98 | candidateMayBuilder.clause(Integer.class, existingContents -> List.of( | 110 | candidateMayBuilder.clause(Integer.class, existingContents -> List.of( |
99 | candidateMust(nodeType.call(node)), | 111 | candidateMust(nodeType.call(node)), |
100 | new CountCandidateUpperBoundLiteral(existingContents, linkType, arguments), | 112 | new CountCandidateUpperBoundLiteral(existingContents, linkType, arguments), |
101 | check(greater(existingContents, IntTerms.constant(upperBound))) | 113 | check(greater(existingContents, constant(upperBound))) |
102 | )); | 114 | )); |
103 | candidateMustBuilder.clause(Integer.class, existingContents -> List.of( | 115 | candidateMustBuilder.clause(Integer.class, existingContents -> List.of( |
104 | candidateMust(nodeType.call(node)), | 116 | candidateMust(nodeType.call(node)), |
105 | new CountCandidateLowerBoundLiteral(existingContents, linkType, arguments), | 117 | new CountCandidateLowerBoundLiteral(existingContents, linkType, arguments), |
106 | check(greater(existingContents, IntTerms.constant(upperBound))) | 118 | check(greater(existingContents, constant(upperBound))) |
119 | )); | ||
120 | missingBuilder.clause(Integer.class, existingContents -> List.of( | ||
121 | candidateMust(nodeType.call(node)), | ||
122 | new CountCandidateUpperBoundLiteral(existingContents, linkType, arguments), | ||
123 | missingOutput.assign(sub(existingContents, constant(upperBound))), | ||
124 | check(greater(missingOutput, constant(0))) | ||
107 | )); | 125 | )); |
108 | } | 126 | } |
109 | 127 | ||
128 | var objective = Query.of(name + "#objective", Integer.class, (builder, output) -> builder.clause( | ||
129 | output.assign(missingBuilder.build().aggregate(INT_SUM, Variable.of())) | ||
130 | )); | ||
131 | |||
110 | storeBuilder.with(PartialRelationTranslator.of(constrainedMultiplicity.errorSymbol()) | 132 | storeBuilder.with(PartialRelationTranslator.of(constrainedMultiplicity.errorSymbol()) |
111 | .mayNever() | 133 | .mayNever() |
112 | .must(mustBuilder.build()) | 134 | .must(mustBuilder.build()) |
113 | .candidateMay(candidateMayBuilder.build()) | 135 | .candidateMay(candidateMayBuilder.build()) |
114 | .candidateMust(candidateMustBuilder.build())); | 136 | .candidateMust(candidateMustBuilder.build()) |
137 | .objective(Objectives.value(objective))); | ||
115 | } | 138 | } |
116 | } | 139 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateTranslator.java index 16745da1..b401118e 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateTranslator.java | |||
@@ -78,7 +78,14 @@ public class PredicateTranslator implements ModelStoreConfiguration { | |||
78 | .clause(mayLiterals) | 78 | .clause(mayLiterals) |
79 | .build(); | 79 | .build(); |
80 | translator.may(may); | 80 | translator.may(may); |
81 | } else if (!defaultValue.may()) { | 81 | } else if (defaultValue.may()) { |
82 | // If all values are permitted, we don't need to check for any forbidden values in the model. | ||
83 | // If the result of this predicate of {@code ERROR}, some other partial relation (that we check for) | ||
84 | // will be {@code ERROR} as well. | ||
85 | translator.exclude(null); | ||
86 | translator.accept(null); | ||
87 | translator.objective(null); | ||
88 | } else { | ||
82 | translator.mayNever(); | 89 | translator.mayNever(); |
83 | } | 90 | } |
84 | storeBuilder.with(translator); | 91 | storeBuilder.with(translator); |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java index 67e8035f..dc8a1d36 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java | |||
@@ -5,16 +5,26 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | 6 | package tools.refinery.store.reasoning.translator.typehierarchy; |
7 | 7 | ||
8 | import tools.refinery.store.dse.transition.Rule; | ||
9 | import tools.refinery.store.dse.transition.actions.ActionLiteral; | ||
8 | import tools.refinery.store.model.ModelStoreBuilder; | 10 | import tools.refinery.store.model.ModelStoreBuilder; |
9 | import tools.refinery.store.model.ModelStoreConfiguration; | 11 | import tools.refinery.store.model.ModelStoreConfiguration; |
10 | import tools.refinery.store.query.dnf.Query; | 12 | import tools.refinery.store.query.dnf.Query; |
11 | import tools.refinery.store.reasoning.ReasoningBuilder; | 13 | import tools.refinery.store.reasoning.ReasoningBuilder; |
14 | import tools.refinery.store.reasoning.actions.PartialActionLiterals; | ||
12 | import tools.refinery.store.reasoning.literal.PartialLiterals; | 15 | import tools.refinery.store.reasoning.literal.PartialLiterals; |
13 | import tools.refinery.store.reasoning.representation.PartialRelation; | 16 | import tools.refinery.store.reasoning.representation.PartialRelation; |
14 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | 17 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; |
18 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
15 | import tools.refinery.store.reasoning.translator.proxy.PartialRelationTranslatorProxy; | 19 | import tools.refinery.store.reasoning.translator.proxy.PartialRelationTranslatorProxy; |
16 | import tools.refinery.store.representation.Symbol; | 20 | import tools.refinery.store.representation.Symbol; |
17 | 21 | ||
22 | import java.util.ArrayList; | ||
23 | |||
24 | import static tools.refinery.store.query.literal.Literals.not; | ||
25 | import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMust; | ||
26 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | ||
27 | |||
18 | public class TypeHierarchyTranslator implements ModelStoreConfiguration { | 28 | public class TypeHierarchyTranslator implements ModelStoreConfiguration { |
19 | private final Symbol<InferredType> typeSymbol = Symbol.of("TYPE", 1, InferredType.class, InferredType.UNTYPED); | 29 | private final Symbol<InferredType> typeSymbol = Symbol.of("TYPE", 1, InferredType.class, InferredType.UNTYPED); |
20 | private final TypeHierarchy typeHierarchy; | 30 | private final TypeHierarchy typeHierarchy; |
@@ -49,7 +59,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { | |||
49 | builder.clause(new MayTypeView(typeSymbol, type).call(p1)); | 59 | builder.clause(new MayTypeView(typeSymbol, type).call(p1)); |
50 | } | 60 | } |
51 | for (var subtype : result.getDirectSubtypes()) { | 61 | for (var subtype : result.getDirectSubtypes()) { |
52 | builder.clause(PartialLiterals.may(subtype.call(p1))); | 62 | builder.clause(may(subtype.call(p1))); |
53 | } | 63 | } |
54 | }); | 64 | }); |
55 | 65 | ||
@@ -66,11 +76,31 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { | |||
66 | } | 76 | } |
67 | }); | 77 | }); |
68 | 78 | ||
69 | return PartialRelationTranslator.of(type) | 79 | var translator = PartialRelationTranslator.of(type) |
70 | .may(may) | 80 | .may(may) |
71 | .must(must) | 81 | .must(must) |
72 | .candidate(candidate) | 82 | .candidate(candidate) |
73 | .refiner(InferredTypeRefiner.of(typeSymbol, result)); | 83 | .refiner(InferredTypeRefiner.of(typeSymbol, result)); |
84 | |||
85 | if (!result.isAbstractType()) { | ||
86 | var decision = Rule.of(type.name(), (builder, instance) -> builder | ||
87 | .clause( | ||
88 | may(type.call(instance)), | ||
89 | not(candidateMust(type.call(instance))), | ||
90 | not(MultiObjectTranslator.MULTI_VIEW.call(instance)) | ||
91 | ) | ||
92 | .action(() -> { | ||
93 | var actionLiterals = new ArrayList<ActionLiteral>(); | ||
94 | actionLiterals.add(PartialActionLiterals.add(type, instance)); | ||
95 | for (var subtype : result.getDirectSubtypes()) { | ||
96 | actionLiterals.add(PartialActionLiterals.remove(subtype, instance)); | ||
97 | } | ||
98 | return actionLiterals; | ||
99 | })); | ||
100 | translator.decision(decision); | ||
101 | } | ||
102 | |||
103 | return translator; | ||
74 | } | 104 | } |
75 | 105 | ||
76 | private ModelStoreConfiguration createEliminatedTypeTranslator( | 106 | private ModelStoreConfiguration createEliminatedTypeTranslator( |