diff options
author | 2023-07-18 20:18:48 +0200 | |
---|---|---|
committer | 2023-07-20 15:54:49 +0200 | |
commit | bc742b20fa187200def2809e5aef71547f75c65a (patch) | |
tree | f12e0344805501118410520ee8a60905a6541210 /subprojects | |
parent | feat: use base index for local search (diff) | |
download | refinery-bc742b20fa187200def2809e5aef71547f75c65a.tar.gz refinery-bc742b20fa187200def2809e5aef71547f75c65a.tar.zst refinery-bc742b20fa187200def2809e5aef71547f75c65a.zip |
feat: basic partial interpretation infrastructure
Diffstat (limited to 'subprojects')
65 files changed, 1968 insertions, 795 deletions
diff --git a/subprojects/store-reasoning/build.gradle.kts b/subprojects/store-reasoning/build.gradle.kts index 6c568df0..5885da83 100644 --- a/subprojects/store-reasoning/build.gradle.kts +++ b/subprojects/store-reasoning/build.gradle.kts | |||
@@ -11,4 +11,5 @@ plugins { | |||
11 | dependencies { | 11 | dependencies { |
12 | api(project(":refinery-store-query")) | 12 | api(project(":refinery-store-query")) |
13 | testImplementation(testFixtures(project(":refinery-store-query"))) | 13 | testImplementation(testFixtures(project(":refinery-store-query"))) |
14 | testImplementation(project(":refinery-store-query-viatra")) | ||
14 | } | 15 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java deleted file mode 100644 index d3a216d8..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java +++ /dev/null | |||
@@ -1,20 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning; | ||
7 | |||
8 | public enum MergeResult { | ||
9 | UNCHANGED, | ||
10 | REFINED, | ||
11 | REJECTED; | ||
12 | |||
13 | public MergeResult andAlso(MergeResult other) { | ||
14 | return switch (this) { | ||
15 | case UNCHANGED -> other; | ||
16 | case REFINED -> other == REJECTED ? REJECTED : REFINED; | ||
17 | case REJECTED -> REJECTED; | ||
18 | }; | ||
19 | } | ||
20 | } | ||
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 66e809f7..17aec09c 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 | |||
@@ -5,27 +5,46 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning; | 6 | package tools.refinery.store.reasoning; |
7 | 7 | ||
8 | import org.jetbrains.annotations.Nullable; | ||
8 | import tools.refinery.store.adapter.ModelAdapter; | 9 | import tools.refinery.store.adapter.ModelAdapter; |
9 | import tools.refinery.store.query.resultset.ResultSet; | 10 | import tools.refinery.store.reasoning.internal.ReasoningBuilderImpl; |
10 | import tools.refinery.store.query.dnf.Dnf; | 11 | import tools.refinery.store.reasoning.interpretation.AnyPartialInterpretation; |
12 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | ||
13 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
14 | import tools.refinery.store.reasoning.refinement.AnyPartialInterpretationRefiner; | ||
15 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
11 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 16 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
12 | import tools.refinery.store.reasoning.representation.PartialRelation; | 17 | import tools.refinery.store.reasoning.representation.PartialRelation; |
13 | import tools.refinery.store.reasoning.representation.PartialSymbol; | 18 | import tools.refinery.store.reasoning.representation.PartialSymbol; |
19 | import tools.refinery.store.tuple.Tuple1; | ||
14 | 20 | ||
15 | public interface ReasoningAdapter extends ModelAdapter { | 21 | public interface ReasoningAdapter extends ModelAdapter { |
16 | PartialRelation EXISTS = PartialSymbol.of("exists", 1); | 22 | PartialRelation EXISTS_SYMBOL = PartialSymbol.of("exists", 1); |
17 | PartialRelation EQUALS = PartialSymbol.of("equals", 2); | 23 | PartialRelation EQUALS_SYMBOL = PartialSymbol.of("equals", 2); |
18 | 24 | ||
19 | @Override | 25 | @Override |
20 | ReasoningStoreAdapter getStoreAdapter(); | 26 | ReasoningStoreAdapter getStoreAdapter(); |
21 | 27 | ||
22 | default AnyPartialInterpretation getPartialInterpretation(AnyPartialSymbol partialSymbol) { | 28 | default AnyPartialInterpretation getPartialInterpretation(Concreteness concreteness, |
23 | // Cast to disambiguate overloads. | 29 | AnyPartialSymbol partialSymbol) { |
24 | var typedPartialSymbol = (PartialSymbol<?, ?>) partialSymbol; | 30 | return getPartialInterpretation(concreteness, (PartialSymbol<?, ?>) partialSymbol); |
25 | return getPartialInterpretation(typedPartialSymbol); | ||
26 | } | 31 | } |
27 | 32 | ||
28 | <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol); | 33 | <A, C> PartialInterpretation<A, C> getPartialInterpretation(Concreteness concreteness, |
34 | PartialSymbol<A, C> partialSymbol); | ||
29 | 35 | ||
30 | ResultSet<Boolean> getLiftedResultSet(Dnf query); | 36 | default AnyPartialInterpretationRefiner getRefiner(AnyPartialSymbol partialSymbol) { |
37 | return getRefiner((PartialSymbol<?, ?>) partialSymbol); | ||
38 | } | ||
39 | |||
40 | <A, C> PartialInterpretationRefiner<A, C> getRefiner(PartialSymbol<A, C> partialSymbol); | ||
41 | |||
42 | @Nullable | ||
43 | Tuple1 split(int parentMultiObject); | ||
44 | |||
45 | boolean cleanup(int nodeToDelete); | ||
46 | |||
47 | static ReasoningBuilder builder() { | ||
48 | return new ReasoningBuilderImpl(); | ||
49 | } | ||
31 | } | 50 | } |
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 d3a337e8..6d416436 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 | |||
@@ -7,26 +7,28 @@ 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.model.ModelStore; | 9 | import tools.refinery.store.model.ModelStore; |
10 | import tools.refinery.store.reasoning.literal.Modality; | ||
11 | import tools.refinery.store.query.dnf.Dnf; | 10 | import tools.refinery.store.query.dnf.Dnf; |
12 | 11 | import tools.refinery.store.query.dnf.Query; | |
13 | import java.util.Collection; | 12 | import tools.refinery.store.reasoning.literal.Concreteness; |
14 | import java.util.List; | 13 | import tools.refinery.store.reasoning.literal.Modality; |
14 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | ||
15 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | ||
16 | import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator; | ||
17 | import tools.refinery.store.representation.Symbol; | ||
15 | 18 | ||
16 | @SuppressWarnings("UnusedReturnValue") | 19 | @SuppressWarnings("UnusedReturnValue") |
17 | public interface ReasoningBuilder extends ModelAdapterBuilder { | 20 | public interface ReasoningBuilder extends ModelAdapterBuilder { |
18 | default ReasoningBuilder liftedQueries(Dnf... liftedQueries) { | 21 | ReasoningBuilder initialNodeCount(int nodeCount); |
19 | return liftedQueries(List.of(liftedQueries)); | 22 | |
20 | } | 23 | ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator); |
24 | |||
25 | <T> ReasoningBuilder storageRefiner(Symbol<T> symbol, StorageRefiner.Factory<T> refiner); | ||
21 | 26 | ||
22 | default ReasoningBuilder liftedQueries(Collection<Dnf> liftedQueries) { | 27 | ReasoningBuilder initializer(PartialModelInitializer initializer); |
23 | liftedQueries.forEach(this::liftedQuery); | ||
24 | return this; | ||
25 | } | ||
26 | 28 | ||
27 | ReasoningBuilder liftedQuery(Dnf liftedQuery); | 29 | <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query); |
28 | 30 | ||
29 | Dnf lift(Modality modality, Dnf query); | 31 | Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf); |
30 | 32 | ||
31 | @Override | 33 | @Override |
32 | ReasoningStoreAdapter build(ModelStore store); | 34 | ReasoningStoreAdapter build(ModelStore store); |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java index c9795255..fae60d9e 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java | |||
@@ -8,14 +8,15 @@ package tools.refinery.store.reasoning; | |||
8 | import tools.refinery.store.adapter.ModelStoreAdapter; | 8 | import tools.refinery.store.adapter.ModelStoreAdapter; |
9 | import tools.refinery.store.model.Model; | 9 | import tools.refinery.store.model.Model; |
10 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 10 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
11 | import tools.refinery.store.query.dnf.Dnf; | ||
12 | 11 | ||
13 | import java.util.Collection; | 12 | import java.util.Collection; |
14 | 13 | ||
15 | public interface ReasoningStoreAdapter extends ModelStoreAdapter { | 14 | public interface ReasoningStoreAdapter extends ModelStoreAdapter { |
16 | Collection<AnyPartialSymbol> getPartialSymbols(); | 15 | Collection<AnyPartialSymbol> getPartialSymbols(); |
17 | 16 | ||
18 | Collection<Dnf> getLiftedQueries(); | 17 | Collection<AnyPartialSymbol> getRefinablePartialSymbols(); |
18 | |||
19 | Model createInitialModel(); | ||
19 | 20 | ||
20 | @Override | 21 | @Override |
21 | ReasoningAdapter createModelAdapter(Model model); | 22 | ReasoningAdapter createModelAdapter(Model model); |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java new file mode 100644 index 00000000..132022d1 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java | |||
@@ -0,0 +1,103 @@ | |||
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.internal; | ||
7 | |||
8 | import tools.refinery.store.query.dnf.Dnf; | ||
9 | import tools.refinery.store.query.dnf.DnfClause; | ||
10 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
11 | import tools.refinery.store.query.literal.Literal; | ||
12 | import tools.refinery.store.query.rewriter.AbstractRecursiveRewriter; | ||
13 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; | ||
14 | import tools.refinery.store.reasoning.lifting.DnfLifter; | ||
15 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
16 | import tools.refinery.store.reasoning.literal.ModalConstraint; | ||
17 | import tools.refinery.store.reasoning.literal.Modality; | ||
18 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
19 | |||
20 | import java.util.*; | ||
21 | |||
22 | class PartialQueryRewriter extends AbstractRecursiveRewriter { | ||
23 | private final DnfLifter lifter; | ||
24 | private final Map<PartialRelation, PartialRelationRewriter> relationRewriterMap = new HashMap<>(); | ||
25 | |||
26 | PartialQueryRewriter(DnfLifter lifter) { | ||
27 | this.lifter = lifter; | ||
28 | } | ||
29 | |||
30 | public void addRelationRewriter(PartialRelation partialRelation, PartialRelationRewriter interpreter) { | ||
31 | if (relationRewriterMap.put(partialRelation, interpreter) != null) { | ||
32 | throw new IllegalArgumentException("Duplicate partial relation: " + partialRelation); | ||
33 | } | ||
34 | } | ||
35 | |||
36 | @Override | ||
37 | protected Dnf doRewrite(Dnf dnf) { | ||
38 | var builder = Dnf.builderFrom(dnf); | ||
39 | for (var clause : dnf.getClauses()) { | ||
40 | builder.clause(rewriteClause(clause)); | ||
41 | } | ||
42 | return builder.build(); | ||
43 | } | ||
44 | |||
45 | private List<Literal> rewriteClause(DnfClause clause) { | ||
46 | var completedLiterals = new ArrayList<Literal>(); | ||
47 | var workList = new ArrayDeque<>(clause.literals()); | ||
48 | while (!workList.isEmpty()) { | ||
49 | var literal = workList.removeFirst(); | ||
50 | rewrite(literal, completedLiterals, workList); | ||
51 | } | ||
52 | return completedLiterals; | ||
53 | } | ||
54 | |||
55 | private void rewrite(Literal literal, List<Literal> completedLiterals, Deque<Literal> workList) { | ||
56 | if (!(literal instanceof AbstractCallLiteral callLiteral)) { | ||
57 | completedLiterals.add(literal); | ||
58 | return; | ||
59 | } | ||
60 | var target = callLiteral.getTarget(); | ||
61 | if (target instanceof Dnf dnf) { | ||
62 | rewriteRecursively(callLiteral, dnf, completedLiterals); | ||
63 | } else if (target instanceof ModalConstraint modalConstraint) { | ||
64 | var modality = modalConstraint.modality(); | ||
65 | var concreteness = modalConstraint.concreteness(); | ||
66 | var constraint = modalConstraint.constraint(); | ||
67 | if (constraint instanceof Dnf dnf) { | ||
68 | rewriteRecursively(callLiteral, modality, concreteness, dnf, completedLiterals); | ||
69 | } else if (constraint instanceof PartialRelation partialRelation) { | ||
70 | rewrite(callLiteral, modality, concreteness, partialRelation, workList); | ||
71 | } else { | ||
72 | throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint); | ||
73 | } | ||
74 | } else { | ||
75 | completedLiterals.add(literal); | ||
76 | } | ||
77 | } | ||
78 | |||
79 | private void rewriteRecursively(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, | ||
80 | Dnf dnf, List<Literal> completedLiterals) { | ||
81 | var liftedDnf = lifter.lift(modality, concreteness, dnf); | ||
82 | rewriteRecursively(callLiteral, liftedDnf, completedLiterals); | ||
83 | } | ||
84 | |||
85 | private void rewriteRecursively(AbstractCallLiteral callLiteral, Dnf dnf, List<Literal> completedLiterals) { | ||
86 | var rewrittenDnf = rewrite(dnf); | ||
87 | var rewrittenLiteral = callLiteral.withTarget(rewrittenDnf); | ||
88 | completedLiterals.add(rewrittenLiteral); | ||
89 | } | ||
90 | |||
91 | private void rewrite(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, | ||
92 | PartialRelation partialRelation, Deque<Literal> workList) { | ||
93 | var rewriter = relationRewriterMap.get(partialRelation); | ||
94 | if (rewriter == null) { | ||
95 | throw new IllegalArgumentException("Do not know how to interpret partial relation: " + partialRelation); | ||
96 | } | ||
97 | var literals = rewriter.rewriteLiteral(callLiteral, modality, concreteness); | ||
98 | int length = literals.size(); | ||
99 | for (int i = length - 1; i >= 0; i--) { | ||
100 | workList.addFirst(literals.get(i)); | ||
101 | } | ||
102 | } | ||
103 | } | ||
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 1bd3ad2e..396c2dcc 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 | |||
@@ -5,20 +5,99 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.internal; | 6 | package tools.refinery.store.reasoning.internal; |
7 | 7 | ||
8 | import org.jetbrains.annotations.Nullable; | ||
9 | import tools.refinery.store.model.Interpretation; | ||
8 | import tools.refinery.store.model.Model; | 10 | import tools.refinery.store.model.Model; |
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | 11 | import tools.refinery.store.reasoning.ReasoningAdapter; |
10 | import tools.refinery.store.reasoning.PartialInterpretation; | 12 | import tools.refinery.store.reasoning.interpretation.AnyPartialInterpretation; |
13 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | ||
14 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
15 | import tools.refinery.store.reasoning.refinement.AnyPartialInterpretationRefiner; | ||
16 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
17 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | ||
18 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
11 | import tools.refinery.store.reasoning.representation.PartialSymbol; | 19 | import tools.refinery.store.reasoning.representation.PartialSymbol; |
12 | import tools.refinery.store.query.dnf.Dnf; | 20 | import tools.refinery.store.representation.Symbol; |
13 | import tools.refinery.store.query.resultset.ResultSet; | 21 | import tools.refinery.store.tuple.Tuple; |
22 | import tools.refinery.store.tuple.Tuple1; | ||
14 | 23 | ||
15 | public class ReasoningAdapterImpl implements ReasoningAdapter { | 24 | import java.util.HashMap; |
25 | import java.util.Map; | ||
26 | |||
27 | class ReasoningAdapterImpl implements ReasoningAdapter { | ||
28 | static final Symbol<Integer> NODE_COUNT_SYMBOL = Symbol.of("MODEL_SIZE", 0, Integer.class, 0); | ||
16 | private final Model model; | 29 | private final Model model; |
17 | private final ReasoningStoreAdapterImpl storeAdapter; | 30 | private final ReasoningStoreAdapterImpl storeAdapter; |
31 | private final Map<AnyPartialSymbol, AnyPartialInterpretation>[] partialInterpretations; | ||
32 | private final Map<AnyPartialSymbol, AnyPartialInterpretationRefiner> refiners; | ||
33 | private final StorageRefiner[] storageRefiners; | ||
34 | private final Interpretation<Integer> nodeCountInterpretation; | ||
18 | 35 | ||
19 | ReasoningAdapterImpl(Model model, ReasoningStoreAdapterImpl storeAdapter) { | 36 | ReasoningAdapterImpl(Model model, ReasoningStoreAdapterImpl storeAdapter) { |
20 | this.model = model; | 37 | this.model = model; |
21 | this.storeAdapter = storeAdapter; | 38 | this.storeAdapter = storeAdapter; |
39 | |||
40 | int concretenessLength = Concreteness.values().length; | ||
41 | // Creation of a generic array. | ||
42 | @SuppressWarnings({"unchecked", "squid:S1905"}) | ||
43 | var interpretationsArray = (Map<AnyPartialSymbol, AnyPartialInterpretation>[]) new Map[concretenessLength]; | ||
44 | partialInterpretations = interpretationsArray; | ||
45 | createPartialInterpretations(); | ||
46 | |||
47 | var refinerFactories = storeAdapter.getSymbolRefiners(); | ||
48 | refiners = new HashMap<>(refinerFactories.size()); | ||
49 | createRefiners(); | ||
50 | |||
51 | storageRefiners = storeAdapter.createRepresentationRefiners(model); | ||
52 | |||
53 | nodeCountInterpretation = model.getInterpretation(NODE_COUNT_SYMBOL); | ||
54 | } | ||
55 | |||
56 | private void createPartialInterpretations() { | ||
57 | int concretenessLength = Concreteness.values().length; | ||
58 | var interpretationFactories = storeAdapter.getSymbolInterpreters(); | ||
59 | for (int i = 0; i < concretenessLength; i++) { | ||
60 | partialInterpretations[i] = new HashMap<>(interpretationFactories.size()); | ||
61 | } | ||
62 | // Create the partial interpretations in order so that factories may refer to interpretations of symbols | ||
63 | // preceding them in the ordered {@code interpretationFactories} map, e.g., for opposite interpretations. | ||
64 | for (var entry : interpretationFactories.entrySet()) { | ||
65 | var partialSymbol = entry.getKey(); | ||
66 | var factory = entry.getValue(); | ||
67 | for (int i = 0; i < concretenessLength; i++) { | ||
68 | var concreteness = Concreteness.values()[i]; | ||
69 | var interpretation = createPartialInterpretation(concreteness, factory, partialSymbol); | ||
70 | partialInterpretations[i].put(partialSymbol, interpretation); | ||
71 | } | ||
72 | } | ||
73 | } | ||
74 | |||
75 | private <A, C> PartialInterpretation<A, C> createPartialInterpretation( | ||
76 | Concreteness concreteness, PartialInterpretation.Factory<A, C> interpreter, AnyPartialSymbol symbol) { | ||
77 | // The builder only allows well-typed assignment of interpreters to symbols. | ||
78 | @SuppressWarnings("unchecked") | ||
79 | var typedSymbol = (PartialSymbol<A, C>) symbol; | ||
80 | return interpreter.create(this, concreteness, typedSymbol); | ||
81 | } | ||
82 | |||
83 | private void createRefiners() { | ||
84 | var refinerFactories = storeAdapter.getSymbolRefiners(); | ||
85 | // Create the partial interpretations refiners in order so that factories may refer to refiners of symbols | ||
86 | // preceding them in the ordered {@code interpretationFactories} map, e.g., for opposite interpretations. | ||
87 | for (var entry : refinerFactories.entrySet()) { | ||
88 | var partialSymbol = entry.getKey(); | ||
89 | var factory = entry.getValue(); | ||
90 | var refiner = createRefiner(factory, partialSymbol); | ||
91 | refiners.put(partialSymbol, refiner); | ||
92 | } | ||
93 | } | ||
94 | |||
95 | private <A, C> PartialInterpretationRefiner<A, C> createRefiner( | ||
96 | PartialInterpretationRefiner.Factory<A, C> factory, AnyPartialSymbol symbol) { | ||
97 | // The builder only allows well-typed assignment of interpreters to symbols. | ||
98 | @SuppressWarnings("unchecked") | ||
99 | var typedSymbol = (PartialSymbol<A, C>) symbol; | ||
100 | return factory.create(this, typedSymbol); | ||
22 | } | 101 | } |
23 | 102 | ||
24 | @Override | 103 | @Override |
@@ -32,12 +111,59 @@ public class ReasoningAdapterImpl implements ReasoningAdapter { | |||
32 | } | 111 | } |
33 | 112 | ||
34 | @Override | 113 | @Override |
35 | public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) { | 114 | public <A, C> PartialInterpretation<A, C> getPartialInterpretation(Concreteness concreteness, |
36 | return null; | 115 | PartialSymbol<A, C> partialSymbol) { |
116 | var map = partialInterpretations[concreteness.ordinal()]; | ||
117 | var interpretation = map.get(partialSymbol); | ||
118 | if (interpretation == null) { | ||
119 | throw new IllegalArgumentException("No interpretation for partial symbol: " + partialSymbol); | ||
120 | } | ||
121 | // The builder only allows well-typed assignment of interpreters to symbols. | ||
122 | @SuppressWarnings("unchecked") | ||
123 | var typedInterpretation = (PartialInterpretation<A, C>) interpretation; | ||
124 | return typedInterpretation; | ||
125 | } | ||
126 | |||
127 | @Override | ||
128 | public <A, C> PartialInterpretationRefiner<A, C> getRefiner(PartialSymbol<A, C> partialSymbol) { | ||
129 | var refiner = refiners.get(partialSymbol); | ||
130 | if (refiner == null) { | ||
131 | throw new IllegalArgumentException("No refiner for partial symbol: " + partialSymbol); | ||
132 | } | ||
133 | // The builder only allows well-typed assignment of refiners to symbols. | ||
134 | @SuppressWarnings("unchecked") | ||
135 | var typedRefiner = (PartialInterpretationRefiner<A, C>) refiner; | ||
136 | return typedRefiner; | ||
137 | } | ||
138 | |||
139 | @Override | ||
140 | @Nullable | ||
141 | public Tuple1 split(int parentNode) { | ||
142 | int newNodeId = nodeCountInterpretation.get(Tuple.of()); | ||
143 | nodeCountInterpretation.put(Tuple.of(), newNodeId + 1); | ||
144 | // Avoid creating an iterator object. | ||
145 | //noinspection ForLoopReplaceableByForEach | ||
146 | for (int i = 0; i < storageRefiners.length; i++) { | ||
147 | if (!storageRefiners[i].split(parentNode, newNodeId)) { | ||
148 | return null; | ||
149 | } | ||
150 | } | ||
151 | return Tuple.of(newNodeId); | ||
37 | } | 152 | } |
38 | 153 | ||
39 | @Override | 154 | @Override |
40 | public ResultSet<Boolean> getLiftedResultSet(Dnf query) { | 155 | public boolean cleanup(int nodeToDelete) { |
41 | return null; | 156 | // Avoid creating an iterator object. |
157 | //noinspection ForLoopReplaceableByForEach | ||
158 | for (int i = 0; i < storageRefiners.length; i++) { | ||
159 | if (!storageRefiners[i].cleanup(nodeToDelete)) { | ||
160 | return false; | ||
161 | } | ||
162 | } | ||
163 | int currentModelSize = nodeCountInterpretation.get(Tuple.of()); | ||
164 | if (nodeToDelete == currentModelSize - 1) { | ||
165 | nodeCountInterpretation.put(Tuple.of(), nodeToDelete); | ||
166 | } | ||
167 | return true; | ||
42 | } | 168 | } |
43 | } | 169 | } |
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 aa71496c..f7a91284 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 | |||
@@ -7,25 +7,138 @@ 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.model.ModelStore; | 9 | import tools.refinery.store.model.ModelStore; |
10 | import tools.refinery.store.model.ModelStoreBuilder; | ||
11 | import tools.refinery.store.query.ModelQueryBuilder; | ||
10 | import tools.refinery.store.query.dnf.Dnf; | 12 | import tools.refinery.store.query.dnf.Dnf; |
13 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.reasoning.ReasoningBuilder; | 14 | import tools.refinery.store.reasoning.ReasoningBuilder; |
15 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | ||
16 | import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner; | ||
17 | import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator; | ||
18 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
19 | import tools.refinery.store.reasoning.lifting.DnfLifter; | ||
20 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
12 | import tools.refinery.store.reasoning.literal.Modality; | 21 | import tools.refinery.store.reasoning.literal.Modality; |
22 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
23 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | ||
24 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | ||
25 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
26 | import tools.refinery.store.representation.AnySymbol; | ||
27 | import tools.refinery.store.representation.Symbol; | ||
28 | |||
29 | import java.util.*; | ||
13 | 30 | ||
14 | public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningStoreAdapterImpl> | 31 | public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningStoreAdapterImpl> |
15 | implements ReasoningBuilder { | 32 | implements ReasoningBuilder { |
33 | private final DnfLifter lifter = new DnfLifter(); | ||
34 | private final PartialQueryRewriter queryRewriter = new PartialQueryRewriter(lifter); | ||
35 | private final Map<AnyPartialSymbol, AnyPartialSymbolTranslator> translators = new LinkedHashMap<>(); | ||
36 | private final Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters = new LinkedHashMap<>(); | ||
37 | private final Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners = | ||
38 | new LinkedHashMap<>(); | ||
39 | private final Map<AnySymbol, StorageRefiner.Factory<?>> registeredStorageRefiners = new LinkedHashMap<>(); | ||
40 | private final List<PartialModelInitializer> initializers = new ArrayList<>(); | ||
41 | private int initialNodeCount = 0; | ||
42 | |||
43 | @Override | ||
44 | public ReasoningBuilder initialNodeCount(int nodeCount) { | ||
45 | if (nodeCount < 0) { | ||
46 | throw new IllegalArgumentException("Initial model size must not be negative"); | ||
47 | } | ||
48 | initialNodeCount = nodeCount; | ||
49 | return this; | ||
50 | } | ||
51 | |||
16 | @Override | 52 | @Override |
17 | public ReasoningBuilder liftedQuery(Dnf liftedQuery) { | 53 | public ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator) { |
18 | return null; | 54 | var partialSymbol = translator.getPartialSymbol(); |
55 | var oldConfiguration = translators.put(partialSymbol, translator); | ||
56 | if (oldConfiguration != null && oldConfiguration != translator) { | ||
57 | throw new IllegalArgumentException("Duplicate configuration for symbol: " + partialSymbol); | ||
58 | } | ||
59 | return this; | ||
19 | } | 60 | } |
20 | 61 | ||
21 | @Override | 62 | @Override |
22 | public Dnf lift(Modality modality, Dnf query) { | 63 | public <T> ReasoningBuilder storageRefiner(Symbol<T> symbol, StorageRefiner.Factory<T> refiner) { |
23 | checkNotConfigured(); | 64 | checkNotConfigured(); |
24 | return null; | 65 | if (registeredStorageRefiners.put(symbol, refiner) != null) { |
66 | throw new IllegalArgumentException("Duplicate representation refiner for symbol: " + symbol); | ||
67 | } | ||
68 | return this; | ||
69 | } | ||
70 | |||
71 | @Override | ||
72 | public ReasoningBuilder initializer(PartialModelInitializer initializer) { | ||
73 | checkNotConfigured(); | ||
74 | initializers.add(initializer); | ||
75 | return this; | ||
76 | } | ||
77 | |||
78 | @Override | ||
79 | public <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query) { | ||
80 | return lifter.lift(modality, concreteness, query); | ||
81 | } | ||
82 | |||
83 | @Override | ||
84 | public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { | ||
85 | return lifter.lift(modality, concreteness, dnf); | ||
86 | } | ||
87 | |||
88 | @Override | ||
89 | protected void doConfigure(ModelStoreBuilder storeBuilder) { | ||
90 | storeBuilder.symbols(ReasoningAdapterImpl.NODE_COUNT_SYMBOL); | ||
91 | for (var translator : translators.values()) { | ||
92 | translator.configure(storeBuilder); | ||
93 | if (translator instanceof PartialRelationTranslator relationConfiguration) { | ||
94 | doConfigure(relationConfiguration); | ||
95 | } else { | ||
96 | throw new IllegalArgumentException("Unknown partial symbol translator %s for partial symbol %s" | ||
97 | .formatted(translator, translator.getPartialSymbol())); | ||
98 | } | ||
99 | } | ||
100 | storeBuilder.symbols(registeredStorageRefiners.keySet()); | ||
101 | var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class); | ||
102 | queryBuilder.rewriter(queryRewriter); | ||
103 | } | ||
104 | |||
105 | private void doConfigure(PartialRelationTranslator relationConfiguration) { | ||
106 | var partialRelation = relationConfiguration.getPartialRelation(); | ||
107 | queryRewriter.addRelationRewriter(partialRelation, relationConfiguration.getRewriter()); | ||
108 | symbolInterpreters.put(partialRelation, relationConfiguration.getInterpretationFactory()); | ||
109 | var refiner = relationConfiguration.getInterpretationRefiner(); | ||
110 | if (refiner != null) { | ||
111 | symbolRefiners.put(partialRelation, refiner); | ||
112 | } | ||
25 | } | 113 | } |
26 | 114 | ||
27 | @Override | 115 | @Override |
28 | public ReasoningStoreAdapterImpl doBuild(ModelStore store) { | 116 | public ReasoningStoreAdapterImpl doBuild(ModelStore store) { |
29 | return null; | 117 | return new ReasoningStoreAdapterImpl(store, initialNodeCount, Collections.unmodifiableMap(symbolInterpreters), |
118 | Collections.unmodifiableMap(symbolRefiners), getStorageRefiners(store), | ||
119 | Collections.unmodifiableList(initializers)); | ||
120 | } | ||
121 | |||
122 | private Map<AnySymbol, StorageRefiner.Factory<?>> getStorageRefiners(ModelStore store) { | ||
123 | var symbols = store.getSymbols(); | ||
124 | var storageRefiners = new LinkedHashMap<AnySymbol, StorageRefiner.Factory<?>>(symbols.size()); | ||
125 | for (var symbol : symbols) { | ||
126 | var refiner = registeredStorageRefiners.remove(symbol); | ||
127 | if (refiner == null) { | ||
128 | if (symbol.arity() == 0) { | ||
129 | // Arity-0 symbols don't need a default refiner, because they are unaffected by object | ||
130 | // creation/removal. Only a custom refiner ({@code refiner != null}) might need to update them. | ||
131 | continue; | ||
132 | } | ||
133 | // By default, copy over all affected tuples on object creation and remove all affected tuples on | ||
134 | // object removal. | ||
135 | refiner = DefaultStorageRefiner.factory(); | ||
136 | } | ||
137 | storageRefiners.put(symbol, refiner); | ||
138 | } | ||
139 | if (!registeredStorageRefiners.isEmpty()) { | ||
140 | throw new IllegalArgumentException("Unused storage refiners: " + registeredStorageRefiners.keySet()); | ||
141 | } | ||
142 | return Collections.unmodifiableMap(storageRefiners); | ||
30 | } | 143 | } |
31 | } | 144 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java index cdddd8d6..e8b581c6 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java | |||
@@ -5,19 +5,45 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.internal; | 6 | package tools.refinery.store.reasoning.internal; |
7 | 7 | ||
8 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
9 | import tools.refinery.store.model.Model; | 8 | import tools.refinery.store.model.Model; |
10 | import tools.refinery.store.model.ModelStore; | 9 | import tools.refinery.store.model.ModelStore; |
10 | import tools.refinery.store.query.ModelQueryAdapter; | ||
11 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
12 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | ||
13 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
14 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | ||
15 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | ||
11 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 16 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
12 | import tools.refinery.store.query.dnf.Dnf; | 17 | import tools.refinery.store.representation.AnySymbol; |
18 | import tools.refinery.store.representation.Symbol; | ||
19 | import tools.refinery.store.tuple.Tuple; | ||
13 | 20 | ||
14 | import java.util.Collection; | 21 | import java.util.Collection; |
22 | import java.util.List; | ||
23 | import java.util.Map; | ||
15 | 24 | ||
16 | public class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { | 25 | class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { |
17 | private final ModelStore store; | 26 | private final ModelStore store; |
27 | private final Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters; | ||
28 | private final Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners; | ||
29 | private final Map<AnySymbol, StorageRefiner.Factory<?>> representationRefiners; | ||
30 | private final Object initialModelLock = new Object(); | ||
31 | private final int initialNodeCount; | ||
32 | private List<PartialModelInitializer> initializers; | ||
33 | private long initialCommitId = Model.NO_STATE_ID; | ||
18 | 34 | ||
19 | ReasoningStoreAdapterImpl(ModelStore store) { | 35 | ReasoningStoreAdapterImpl(ModelStore store, |
36 | int initialNodeCount, | ||
37 | Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters, | ||
38 | Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners, | ||
39 | Map<AnySymbol, StorageRefiner.Factory<?>> representationRefiners, | ||
40 | List<PartialModelInitializer> initializers) { | ||
20 | this.store = store; | 41 | this.store = store; |
42 | this.initialNodeCount = initialNodeCount; | ||
43 | this.symbolInterpreters = symbolInterpreters; | ||
44 | this.symbolRefiners = symbolRefiners; | ||
45 | this.representationRefiners = representationRefiners; | ||
46 | this.initializers = initializers; | ||
21 | } | 47 | } |
22 | 48 | ||
23 | @Override | 49 | @Override |
@@ -27,12 +53,65 @@ public class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { | |||
27 | 53 | ||
28 | @Override | 54 | @Override |
29 | public Collection<AnyPartialSymbol> getPartialSymbols() { | 55 | public Collection<AnyPartialSymbol> getPartialSymbols() { |
30 | return null; | 56 | return symbolInterpreters.keySet(); |
31 | } | 57 | } |
32 | 58 | ||
33 | @Override | 59 | @Override |
34 | public Collection<Dnf> getLiftedQueries() { | 60 | public Collection<AnyPartialSymbol> getRefinablePartialSymbols() { |
35 | return null; | 61 | return symbolRefiners.keySet(); |
62 | } | ||
63 | |||
64 | // Use of wildcard return value only in internal method not exposed as API, so there is less chance of confusion. | ||
65 | @SuppressWarnings("squid:S1452") | ||
66 | Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> getSymbolInterpreters() { | ||
67 | return symbolInterpreters; | ||
68 | } | ||
69 | |||
70 | // Use of wildcard return value only in internal method not exposed as API, so there is less chance of confusion. | ||
71 | @SuppressWarnings("squid:S1452") | ||
72 | Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> getSymbolRefiners() { | ||
73 | return symbolRefiners; | ||
74 | } | ||
75 | |||
76 | StorageRefiner[] createRepresentationRefiners(Model model) { | ||
77 | var refiners = new StorageRefiner[representationRefiners.size()]; | ||
78 | int i = 0; | ||
79 | for (var entry : representationRefiners.entrySet()) { | ||
80 | var symbol = entry.getKey(); | ||
81 | var factory = entry.getValue(); | ||
82 | refiners[i] = createRepresentationRefiner(factory, model, symbol); | ||
83 | } | ||
84 | return refiners; | ||
85 | } | ||
86 | |||
87 | private <T> StorageRefiner createRepresentationRefiner( | ||
88 | StorageRefiner.Factory<T> factory, Model model, AnySymbol symbol) { | ||
89 | // The builder only allows well-typed assignment of refiners to symbols. | ||
90 | @SuppressWarnings("unchecked") | ||
91 | var typedSymbol = (Symbol<T>) symbol; | ||
92 | return factory.create(typedSymbol, model); | ||
93 | } | ||
94 | |||
95 | @Override | ||
96 | public Model createInitialModel() { | ||
97 | synchronized (initialModelLock) { | ||
98 | if (initialCommitId == Model.NO_STATE_ID) { | ||
99 | return doCreateInitialModel(); | ||
100 | } | ||
101 | return store.createModelForState(initialCommitId); | ||
102 | } | ||
103 | } | ||
104 | |||
105 | private Model doCreateInitialModel() { | ||
106 | var model = store.createEmptyModel(); | ||
107 | model.getInterpretation(ReasoningAdapterImpl.NODE_COUNT_SYMBOL).put(Tuple.of(), initialNodeCount); | ||
108 | for (var initializer : initializers) { | ||
109 | initializer.initialize(model, initialNodeCount); | ||
110 | } | ||
111 | model.getAdapter(ModelQueryAdapter.class).flushChanges(); | ||
112 | initialCommitId = model.commit(); | ||
113 | initializers = null; | ||
114 | return model; | ||
36 | } | 115 | } |
37 | 116 | ||
38 | @Override | 117 | @Override |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.java new file mode 100644 index 00000000..ed291eac --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AbstractPartialInterpretation.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.interpretation; | ||
7 | |||
8 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
9 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
10 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
11 | |||
12 | public abstract class AbstractPartialInterpretation<A, C> implements PartialInterpretation<A, C> { | ||
13 | private final ReasoningAdapter adapter; | ||
14 | private final PartialSymbol<A, C> partialSymbol; | ||
15 | private final Concreteness concreteness; | ||
16 | |||
17 | protected AbstractPartialInterpretation(ReasoningAdapter adapter, Concreteness concreteness, | ||
18 | PartialSymbol<A, C> partialSymbol) { | ||
19 | this.adapter = adapter; | ||
20 | this.partialSymbol = partialSymbol; | ||
21 | this.concreteness = concreteness; | ||
22 | } | ||
23 | |||
24 | @Override | ||
25 | public ReasoningAdapter getAdapter() { | ||
26 | return adapter; | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | public PartialSymbol<A, C> getPartialSymbol() { | ||
31 | return partialSymbol; | ||
32 | } | ||
33 | |||
34 | @Override | ||
35 | public Concreteness getConcreteness() { | ||
36 | return concreteness; | ||
37 | } | ||
38 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AnyPartialInterpretation.java index 000171a1..cd709bc4 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/AnyPartialInterpretation.java | |||
@@ -3,8 +3,10 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning; | 6 | package tools.refinery.store.reasoning.interpretation; |
7 | 7 | ||
8 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
9 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
8 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 10 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
9 | 11 | ||
10 | public sealed interface AnyPartialInterpretation permits PartialInterpretation { | 12 | public sealed interface AnyPartialInterpretation permits PartialInterpretation { |
@@ -12,7 +14,5 @@ public sealed interface AnyPartialInterpretation permits PartialInterpretation { | |||
12 | 14 | ||
13 | AnyPartialSymbol getPartialSymbol(); | 15 | AnyPartialSymbol getPartialSymbol(); |
14 | 16 | ||
15 | int countUnfinished(); | 17 | Concreteness getConcreteness(); |
16 | |||
17 | int countErrors(); | ||
18 | } | 18 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java index 4140d640..3d3d6056 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialInterpretation.java | |||
@@ -3,10 +3,12 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning; | 6 | package tools.refinery.store.reasoning.interpretation; |
7 | 7 | ||
8 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
9 | import tools.refinery.store.map.Cursor; | 8 | import tools.refinery.store.map.Cursor; |
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
11 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
10 | import tools.refinery.store.tuple.Tuple; | 12 | import tools.refinery.store.tuple.Tuple; |
11 | 13 | ||
12 | public non-sealed interface PartialInterpretation<A, C> extends AnyPartialInterpretation { | 14 | public non-sealed interface PartialInterpretation<A, C> extends AnyPartialInterpretation { |
@@ -17,9 +19,8 @@ public non-sealed interface PartialInterpretation<A, C> extends AnyPartialInterp | |||
17 | 19 | ||
18 | Cursor<Tuple, A> getAll(); | 20 | Cursor<Tuple, A> getAll(); |
19 | 21 | ||
20 | MergeResult merge(Tuple key, A value); | 22 | interface Factory<A, C> { |
21 | 23 | PartialInterpretation<A, C> create(ReasoningAdapter adapter, Concreteness concreteness, | |
22 | C getConcrete(Tuple key); | 24 | PartialSymbol<A, C> partialSymbol); |
23 | 25 | } | |
24 | Cursor<Tuple, C> getAllConcrete(); | ||
25 | } | 26 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java new file mode 100644 index 00000000..da8ae0a8 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java | |||
@@ -0,0 +1,17 @@ | |||
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.interpretation; | ||
7 | |||
8 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
9 | import tools.refinery.store.query.literal.Literal; | ||
10 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
11 | import tools.refinery.store.reasoning.literal.Modality; | ||
12 | |||
13 | import java.util.List; | ||
14 | |||
15 | public interface PartialRelationRewriter { | ||
16 | List<Literal> rewriteLiteral(AbstractCallLiteral literal, Modality modality, Concreteness concreteness); | ||
17 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java new file mode 100644 index 00000000..2535714a --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationInterpretationFactory.java | |||
@@ -0,0 +1,180 @@ | |||
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.interpretation; | ||
7 | |||
8 | import tools.refinery.store.map.Cursor; | ||
9 | import tools.refinery.store.query.ModelQueryAdapter; | ||
10 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.query.resultset.ResultSet; | ||
12 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
13 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
14 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
15 | import tools.refinery.store.representation.TruthValue; | ||
16 | import tools.refinery.store.tuple.Tuple; | ||
17 | |||
18 | public class QueryBasedRelationInterpretationFactory implements PartialInterpretation.Factory<TruthValue, Boolean> { | ||
19 | private final Query<Boolean> may; | ||
20 | private final Query<Boolean> must; | ||
21 | private final Query<Boolean> candidateMay; | ||
22 | private final Query<Boolean> candidateMust; | ||
23 | |||
24 | public QueryBasedRelationInterpretationFactory( | ||
25 | Query<Boolean> may, Query<Boolean> must, Query<Boolean> candidateMay, Query<Boolean> candidateMust) { | ||
26 | this.may = may; | ||
27 | this.must = must; | ||
28 | this.candidateMay = candidateMay; | ||
29 | this.candidateMust = candidateMust; | ||
30 | } | ||
31 | |||
32 | @Override | ||
33 | public PartialInterpretation<TruthValue, Boolean> create( | ||
34 | ReasoningAdapter adapter, Concreteness concreteness, PartialSymbol<TruthValue, Boolean> partialSymbol) { | ||
35 | var queryEngine = adapter.getModel().getAdapter(ModelQueryAdapter.class); | ||
36 | ResultSet<Boolean> mayResultSet; | ||
37 | ResultSet<Boolean> mustResultSet; | ||
38 | switch (concreteness) { | ||
39 | case PARTIAL -> { | ||
40 | mayResultSet = queryEngine.getResultSet(may); | ||
41 | mustResultSet = queryEngine.getResultSet(must); | ||
42 | } | ||
43 | case CANDIDATE -> { | ||
44 | mayResultSet = queryEngine.getResultSet(candidateMay); | ||
45 | mustResultSet = queryEngine.getResultSet(candidateMust); | ||
46 | } | ||
47 | default -> throw new IllegalArgumentException("Unknown concreteness: " + concreteness); | ||
48 | } | ||
49 | if (mayResultSet.equals(mustResultSet)) { | ||
50 | return new TwoValuedInterpretation(adapter, concreteness, partialSymbol, mustResultSet); | ||
51 | } else { | ||
52 | return new FourValuedInterpretation( | ||
53 | adapter, concreteness, partialSymbol, mayResultSet, mustResultSet); | ||
54 | } | ||
55 | } | ||
56 | |||
57 | private static class TwoValuedInterpretation extends AbstractPartialInterpretation<TruthValue, Boolean> { | ||
58 | private final ResultSet<Boolean> resultSet; | ||
59 | |||
60 | protected TwoValuedInterpretation( | ||
61 | ReasoningAdapter adapter, Concreteness concreteness, PartialSymbol<TruthValue, Boolean> partialSymbol, | ||
62 | ResultSet<Boolean> resultSet) { | ||
63 | super(adapter, concreteness, partialSymbol); | ||
64 | this.resultSet = resultSet; | ||
65 | } | ||
66 | |||
67 | @Override | ||
68 | public TruthValue get(Tuple key) { | ||
69 | return TruthValue.toTruthValue(resultSet.get(key)); | ||
70 | } | ||
71 | |||
72 | @Override | ||
73 | public Cursor<Tuple, TruthValue> getAll() { | ||
74 | return new TwoValuedCursor(resultSet.getAll()); | ||
75 | } | ||
76 | |||
77 | private record TwoValuedCursor(Cursor<Tuple, Boolean> cursor) implements Cursor<Tuple, TruthValue> { | ||
78 | @Override | ||
79 | public Tuple getKey() { | ||
80 | return cursor.getKey(); | ||
81 | } | ||
82 | |||
83 | @Override | ||
84 | public TruthValue getValue() { | ||
85 | return TruthValue.toTruthValue(cursor.getValue()); | ||
86 | } | ||
87 | |||
88 | @Override | ||
89 | public boolean isTerminated() { | ||
90 | return cursor.isTerminated(); | ||
91 | } | ||
92 | |||
93 | @Override | ||
94 | public boolean move() { | ||
95 | return cursor.move(); | ||
96 | } | ||
97 | } | ||
98 | } | ||
99 | |||
100 | private static class FourValuedInterpretation extends AbstractPartialInterpretation<TruthValue, Boolean> { | ||
101 | private final ResultSet<Boolean> mayResultSet; | ||
102 | private final ResultSet<Boolean> mustResultSet; | ||
103 | |||
104 | public FourValuedInterpretation( | ||
105 | ReasoningAdapter adapter, Concreteness concreteness, PartialSymbol<TruthValue, Boolean> partialSymbol, | ||
106 | ResultSet<Boolean> mayResultSet, ResultSet<Boolean> mustResultSet) { | ||
107 | super(adapter, concreteness, partialSymbol); | ||
108 | this.mayResultSet = mayResultSet; | ||
109 | this.mustResultSet = mustResultSet; | ||
110 | } | ||
111 | |||
112 | @Override | ||
113 | public TruthValue get(Tuple key) { | ||
114 | boolean isMay = mayResultSet.get(key); | ||
115 | boolean isMust = mustResultSet.get(key); | ||
116 | if (isMust) { | ||
117 | return isMay ? TruthValue.TRUE : TruthValue.ERROR; | ||
118 | } else { | ||
119 | return isMay ? TruthValue.UNKNOWN : TruthValue.FALSE; | ||
120 | } | ||
121 | } | ||
122 | |||
123 | @Override | ||
124 | public Cursor<Tuple, TruthValue> getAll() { | ||
125 | return new FourValuedCursor(); | ||
126 | } | ||
127 | |||
128 | private final class FourValuedCursor implements Cursor<Tuple, TruthValue> { | ||
129 | private final Cursor<Tuple, Boolean> mayCursor; | ||
130 | private Cursor<Tuple, Boolean> mustCursor; | ||
131 | |||
132 | private FourValuedCursor() { | ||
133 | this.mayCursor = mayResultSet.getAll(); | ||
134 | } | ||
135 | |||
136 | @Override | ||
137 | public Tuple getKey() { | ||
138 | return mustCursor == null ? mayCursor.getKey() : mustCursor.getKey(); | ||
139 | } | ||
140 | |||
141 | @Override | ||
142 | public TruthValue getValue() { | ||
143 | if (mustCursor != null) { | ||
144 | return TruthValue.ERROR; | ||
145 | } | ||
146 | if (Boolean.TRUE.equals(mustResultSet.get(mayCursor.getKey()))) { | ||
147 | return TruthValue.TRUE; | ||
148 | } | ||
149 | return TruthValue.UNKNOWN; | ||
150 | } | ||
151 | |||
152 | @Override | ||
153 | public boolean isTerminated() { | ||
154 | return mustCursor != null && mustCursor.isTerminated(); | ||
155 | } | ||
156 | |||
157 | @Override | ||
158 | public boolean move() { | ||
159 | if (mayCursor.isTerminated()) { | ||
160 | return moveMust(); | ||
161 | } | ||
162 | if (mayCursor.move()) { | ||
163 | return true; | ||
164 | } | ||
165 | mustCursor = mustResultSet.getAll(); | ||
166 | return moveMust(); | ||
167 | } | ||
168 | |||
169 | private boolean moveMust() { | ||
170 | while (mustCursor.move()) { | ||
171 | // We already iterated over {@code TRUE} truth values with {@code mayCursor}. | ||
172 | if (!Boolean.TRUE.equals(mayResultSet.get(mustCursor.getKey()))) { | ||
173 | return true; | ||
174 | } | ||
175 | } | ||
176 | return false; | ||
177 | } | ||
178 | } | ||
179 | } | ||
180 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java new file mode 100644 index 00000000..3be9e9ac --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java | |||
@@ -0,0 +1,44 @@ | |||
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.interpretation; | ||
7 | |||
8 | import tools.refinery.store.query.dnf.Query; | ||
9 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
10 | import tools.refinery.store.query.literal.Literal; | ||
11 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
12 | import tools.refinery.store.reasoning.literal.Modality; | ||
13 | |||
14 | import java.util.List; | ||
15 | |||
16 | public class QueryBasedRelationRewriter implements PartialRelationRewriter { | ||
17 | private final Query<Boolean> may; | ||
18 | private final Query<Boolean> must; | ||
19 | private final Query<Boolean> candidateMay; | ||
20 | private final Query<Boolean> candidateMust; | ||
21 | |||
22 | public QueryBasedRelationRewriter(Query<Boolean> may, Query<Boolean> must, Query<Boolean> candidateMay, | ||
23 | Query<Boolean> candidateMust) { | ||
24 | this.may = may; | ||
25 | this.must = must; | ||
26 | this.candidateMay = candidateMay; | ||
27 | this.candidateMust = candidateMust; | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public List<Literal> rewriteLiteral(AbstractCallLiteral literal, Modality modality, Concreteness concreteness) { | ||
32 | var query = switch (concreteness) { | ||
33 | case PARTIAL -> switch (modality) { | ||
34 | case MAY -> may; | ||
35 | case MUST -> must; | ||
36 | }; | ||
37 | case CANDIDATE -> switch (modality) { | ||
38 | case MAY -> candidateMay; | ||
39 | case MUST -> candidateMust; | ||
40 | }; | ||
41 | }; | ||
42 | return List.of(literal.withTarget(query.getDnf())); | ||
43 | } | ||
44 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java index d3b0ace8..7bf092a3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ClauseLifter.java | |||
@@ -54,7 +54,7 @@ class ClauseLifter { | |||
54 | var liftedLiteral = liftLiteral(literal); | 54 | var liftedLiteral = liftLiteral(literal); |
55 | liftedLiterals.add(liftedLiteral); | 55 | liftedLiterals.add(liftedLiteral); |
56 | } | 56 | } |
57 | var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); | 57 | var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS_SYMBOL); |
58 | for (var quantifiedVariable : existentialQuantifiersToAdd) { | 58 | for (var quantifiedVariable : existentialQuantifiersToAdd) { |
59 | liftedLiterals.add(existsConstraint.call(quantifiedVariable)); | 59 | liftedLiterals.add(existsConstraint.call(quantifiedVariable)); |
60 | } | 60 | } |
@@ -117,7 +117,7 @@ class ClauseLifter { | |||
117 | var liftedConstraint = ModalConstraint.of(negatedModality, concreteness, target); | 117 | var liftedConstraint = ModalConstraint.of(negatedModality, concreteness, target); |
118 | literals.add(liftedConstraint.call(CallPolarity.POSITIVE, originalArguments)); | 118 | literals.add(liftedConstraint.call(CallPolarity.POSITIVE, originalArguments)); |
119 | 119 | ||
120 | var existsConstraint = ModalConstraint.of(negatedModality, concreteness, ReasoningAdapter.EXISTS); | 120 | var existsConstraint = ModalConstraint.of(negatedModality, concreteness, ReasoningAdapter.EXISTS_SYMBOL); |
121 | for (var variable : uniqueOriginalArguments) { | 121 | for (var variable : uniqueOriginalArguments) { |
122 | if (privateVariables.contains(variable)) { | 122 | if (privateVariables.contains(variable)) { |
123 | literals.add(existsConstraint.call(variable)); | 123 | literals.add(existsConstraint.call(variable)); |
@@ -134,7 +134,7 @@ class ClauseLifter { | |||
134 | var originalArguments = callLiteral.getArguments(); | 134 | var originalArguments = callLiteral.getArguments(); |
135 | var liftedTarget = ModalConstraint.of(modality, concreteness, target); | 135 | var liftedTarget = ModalConstraint.of(modality, concreteness, target); |
136 | 136 | ||
137 | var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS); | 137 | var existsConstraint = ModalConstraint.of(modality, concreteness, ReasoningAdapter.EXISTS_SYMBOL); |
138 | var existingEndHelperName = "%s#exisitingEnd#%s#%s".formatted(target.name(), modality, concreteness); | 138 | var existingEndHelperName = "%s#exisitingEnd#%s#%s".formatted(target.name(), modality, concreteness); |
139 | var existingEndHelper = Dnf.of(existingEndHelperName, builder -> { | 139 | var existingEndHelper = Dnf.of(existingEndHelperName, builder -> { |
140 | var start = builder.parameter("start"); | 140 | var start = builder.parameter("start"); |
@@ -171,10 +171,10 @@ class ClauseLifter { | |||
171 | 171 | ||
172 | private Literal liftEquivalenceLiteral(EquivalenceLiteral equivalenceLiteral) { | 172 | private Literal liftEquivalenceLiteral(EquivalenceLiteral equivalenceLiteral) { |
173 | if (equivalenceLiteral.isPositive()) { | 173 | if (equivalenceLiteral.isPositive()) { |
174 | return ModalConstraint.of(modality, concreteness, ReasoningAdapter.EQUALS) | 174 | return ModalConstraint.of(modality, concreteness, ReasoningAdapter.EQUALS_SYMBOL) |
175 | .call(CallPolarity.POSITIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); | 175 | .call(CallPolarity.POSITIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); |
176 | } | 176 | } |
177 | return ModalConstraint.of(modality.negate(), concreteness, ReasoningAdapter.EQUALS) | 177 | return ModalConstraint.of(modality.negate(), concreteness, ReasoningAdapter.EQUALS_SYMBOL) |
178 | .call(CallPolarity.NEGATIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); | 178 | .call(CallPolarity.NEGATIVE, equivalenceLiteral.getLeft(), equivalenceLiteral.getRight()); |
179 | } | 179 | } |
180 | } | 180 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java index c3b23b43..2e68fa3e 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java | |||
@@ -7,6 +7,7 @@ package tools.refinery.store.reasoning.lifting; | |||
7 | 7 | ||
8 | import tools.refinery.store.query.dnf.Dnf; | 8 | import tools.refinery.store.query.dnf.Dnf; |
9 | import tools.refinery.store.query.dnf.DnfClause; | 9 | import tools.refinery.store.query.dnf.DnfClause; |
10 | import tools.refinery.store.query.dnf.Query; | ||
10 | import tools.refinery.store.query.equality.DnfEqualityChecker; | 11 | import tools.refinery.store.query.equality.DnfEqualityChecker; |
11 | import tools.refinery.store.query.literal.Literal; | 12 | import tools.refinery.store.query.literal.Literal; |
12 | import tools.refinery.store.reasoning.literal.Concreteness; | 13 | import tools.refinery.store.reasoning.literal.Concreteness; |
@@ -19,6 +20,11 @@ import java.util.Map; | |||
19 | public class DnfLifter { | 20 | public class DnfLifter { |
20 | private final Map<ModalDnf, Dnf> cache = new HashMap<>(); | 21 | private final Map<ModalDnf, Dnf> cache = new HashMap<>(); |
21 | 22 | ||
23 | public <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query) { | ||
24 | var liftedDnf = lift(modality, concreteness, query.getDnf()); | ||
25 | return query.withDnf(liftedDnf); | ||
26 | } | ||
27 | |||
22 | public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { | 28 | public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { |
23 | return cache.computeIfAbsent(new ModalDnf(modality, concreteness, dnf), this::doLift); | 29 | return cache.computeIfAbsent(new ModalDnf(modality, concreteness, dnf), this::doLift); |
24 | } | 30 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java index 4f07f17d..2c879397 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java | |||
@@ -13,20 +13,28 @@ public final class PartialLiterals { | |||
13 | } | 13 | } |
14 | 14 | ||
15 | public static CallLiteral may(CallLiteral literal) { | 15 | public static CallLiteral may(CallLiteral literal) { |
16 | return addModality(literal, Modality.MAY); | 16 | return addModality(literal, Modality.MAY, Concreteness.PARTIAL); |
17 | } | 17 | } |
18 | 18 | ||
19 | public static CallLiteral must(CallLiteral literal) { | 19 | public static CallLiteral must(CallLiteral literal) { |
20 | return addModality(literal, Modality.MUST); | 20 | return addModality(literal, Modality.MUST, Concreteness.PARTIAL); |
21 | } | 21 | } |
22 | 22 | ||
23 | public static CallLiteral addModality(CallLiteral literal, Modality modality) { | 23 | public static CallLiteral candidateMay(CallLiteral literal) { |
24 | return addModality(literal, Modality.MAY, Concreteness.CANDIDATE); | ||
25 | } | ||
26 | |||
27 | public static CallLiteral candidateMust(CallLiteral literal) { | ||
28 | return addModality(literal, Modality.MUST, Concreteness.CANDIDATE); | ||
29 | } | ||
30 | |||
31 | public static CallLiteral addModality(CallLiteral literal, Modality modality, Concreteness concreteness) { | ||
24 | var target = literal.getTarget(); | 32 | var target = literal.getTarget(); |
25 | if (target instanceof ModalConstraint) { | 33 | if (target instanceof ModalConstraint) { |
26 | throw new IllegalArgumentException("Literal %s already has modality".formatted(literal)); | 34 | throw new IllegalArgumentException("Literal %s already has modality".formatted(literal)); |
27 | } | 35 | } |
28 | var polarity = literal.getPolarity(); | 36 | var polarity = literal.getPolarity(); |
29 | var modalTarget = new ModalConstraint(modality.commute(polarity), target); | 37 | var modalTarget = new ModalConstraint(modality.commute(polarity), concreteness, target); |
30 | return new CallLiteral(polarity, modalTarget, literal.getArguments()); | 38 | return new CallLiteral(polarity, modalTarget, literal.getArguments()); |
31 | } | 39 | } |
32 | } | 40 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AnyPartialInterpretationRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AnyPartialInterpretationRefiner.java new file mode 100644 index 00000000..6c381511 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AnyPartialInterpretationRefiner.java | |||
@@ -0,0 +1,15 @@ | |||
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.refinement; | ||
7 | |||
8 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
9 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
10 | |||
11 | public sealed interface AnyPartialInterpretationRefiner permits PartialInterpretationRefiner { | ||
12 | ReasoningAdapter getAdapter(); | ||
13 | |||
14 | AnyPartialSymbol getPartialSymbol(); | ||
15 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java new file mode 100644 index 00000000..756118a0 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java | |||
@@ -0,0 +1,51 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.refinement; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
11 | import tools.refinery.store.representation.Symbol; | ||
12 | import tools.refinery.store.tuple.Tuple; | ||
13 | |||
14 | import java.util.Objects; | ||
15 | |||
16 | public class ConcreteSymbolRefiner<A, C> implements PartialInterpretationRefiner<A, C> { | ||
17 | private final ReasoningAdapter adapter; | ||
18 | private final PartialSymbol<A, C> partialSymbol; | ||
19 | private final Interpretation<A> interpretation; | ||
20 | |||
21 | public ConcreteSymbolRefiner(ReasoningAdapter adapter, PartialSymbol<A, C> partialSymbol, | ||
22 | Symbol<A> concreteSymbol) { | ||
23 | this.adapter = adapter; | ||
24 | this.partialSymbol = partialSymbol; | ||
25 | interpretation = adapter.getModel().getInterpretation(concreteSymbol); | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public ReasoningAdapter getAdapter() { | ||
30 | return adapter; | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public PartialSymbol<A, C> getPartialSymbol() { | ||
35 | return partialSymbol; | ||
36 | } | ||
37 | |||
38 | @Override | ||
39 | public boolean merge(Tuple key, A value) { | ||
40 | var currentValue = interpretation.get(key); | ||
41 | var mergedValue = partialSymbol.abstractDomain().commonRefinement(currentValue, value); | ||
42 | if (!Objects.equals(currentValue, mergedValue)) { | ||
43 | interpretation.put(key, mergedValue); | ||
44 | } | ||
45 | return true; | ||
46 | } | ||
47 | |||
48 | public static <A1, C1> PartialInterpretationRefiner.Factory<A1, C1> of(Symbol<A1> concreteSymbol) { | ||
49 | return (adapter, partialSymbol) -> new ConcreteSymbolRefiner<>(adapter, partialSymbol, concreteSymbol); | ||
50 | } | ||
51 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java new file mode 100644 index 00000000..0d7d6c5c --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java | |||
@@ -0,0 +1,80 @@ | |||
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.refinement; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | import tools.refinery.store.tuple.Tuple; | ||
10 | |||
11 | public class DefaultStorageRefiner<T> implements StorageRefiner { | ||
12 | private static final StorageRefiner.Factory<Object> FACTORY = (symbol, model) -> { | ||
13 | var interpretation = model.getInterpretation(symbol); | ||
14 | return new DefaultStorageRefiner<>(interpretation); | ||
15 | }; | ||
16 | |||
17 | private final Interpretation<T> interpretation; | ||
18 | |||
19 | public DefaultStorageRefiner(Interpretation<T> interpretation) { | ||
20 | this.interpretation = interpretation; | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public boolean split(int parentNode, int childNode) { | ||
25 | var symbol = interpretation.getSymbol(); | ||
26 | int arity = symbol.arity(); | ||
27 | for (int i = 0; i < arity; i++) { | ||
28 | int adjacentSize = interpretation.getAdjacentSize(i, parentNode); | ||
29 | if (adjacentSize == 0) { | ||
30 | continue; | ||
31 | } | ||
32 | var toSetKeys = new Tuple[adjacentSize]; | ||
33 | // This is safe, because we won't pass the array to the outside. | ||
34 | @SuppressWarnings("unchecked") | ||
35 | var toSetValues = (T[]) new Object[adjacentSize]; | ||
36 | var cursor = interpretation.getAdjacent(i, parentNode); | ||
37 | int j = 0; | ||
38 | while (cursor.move()) { | ||
39 | toSetKeys[j] = cursor.getKey().set(i, childNode); | ||
40 | toSetValues[j] = cursor.getValue(); | ||
41 | j++; | ||
42 | } | ||
43 | for (j = 0; j < adjacentSize; j++) { | ||
44 | interpretation.put(toSetKeys[j], toSetValues[j]); | ||
45 | } | ||
46 | } | ||
47 | return true; | ||
48 | } | ||
49 | |||
50 | @Override | ||
51 | public boolean cleanup(int nodeToDelete) { | ||
52 | var symbol = interpretation.getSymbol(); | ||
53 | int arity = symbol.arity(); | ||
54 | var defaultValue = symbol.defaultValue(); | ||
55 | for (int i = 0; i < arity; i++) { | ||
56 | int adjacentSize = interpretation.getAdjacentSize(i, nodeToDelete); | ||
57 | if (adjacentSize == 0) { | ||
58 | continue; | ||
59 | } | ||
60 | var toDelete = new Tuple[adjacentSize]; | ||
61 | var cursor = interpretation.getAdjacent(i, nodeToDelete); | ||
62 | int j = 0; | ||
63 | while (cursor.move()) { | ||
64 | toDelete[j] = cursor.getKey(); | ||
65 | j++; | ||
66 | } | ||
67 | for (j = 0; j < adjacentSize; j++) { | ||
68 | interpretation.put(toDelete[j], defaultValue); | ||
69 | } | ||
70 | } | ||
71 | return true; | ||
72 | } | ||
73 | |||
74 | public static <T> StorageRefiner.Factory<T> factory() { | ||
75 | // This is safe, because {@code FACTORY} doesn't depend on {@code T} at all. | ||
76 | @SuppressWarnings("unchecked") | ||
77 | var typedFactory = (StorageRefiner.Factory<T>) FACTORY; | ||
78 | return typedFactory; | ||
79 | } | ||
80 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialInterpretationRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialInterpretationRefiner.java new file mode 100644 index 00000000..f48d1d1f --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialInterpretationRefiner.java | |||
@@ -0,0 +1,22 @@ | |||
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.refinement; | ||
7 | |||
8 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
9 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | public non-sealed interface PartialInterpretationRefiner<A, C> extends AnyPartialInterpretationRefiner { | ||
13 | @Override | ||
14 | PartialSymbol<A, C> getPartialSymbol(); | ||
15 | |||
16 | boolean merge(Tuple key, A value); | ||
17 | |||
18 | @FunctionalInterface | ||
19 | interface Factory<A, C> { | ||
20 | PartialInterpretationRefiner<A, C> create(ReasoningAdapter adapter, PartialSymbol<A, C> partialSymbol); | ||
21 | } | ||
22 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java new file mode 100644 index 00000000..79c1670f --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java | |||
@@ -0,0 +1,13 @@ | |||
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.refinement; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | |||
10 | @FunctionalInterface | ||
11 | public interface PartialModelInitializer { | ||
12 | void initialize(Model model, int nodeCount); | ||
13 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/StorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/StorageRefiner.java new file mode 100644 index 00000000..004696fd --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/StorageRefiner.java | |||
@@ -0,0 +1,20 @@ | |||
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.refinement; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.representation.Symbol; | ||
10 | |||
11 | public interface StorageRefiner { | ||
12 | boolean split(int parentNode, int childNode); | ||
13 | |||
14 | boolean cleanup(int nodeToDelete); | ||
15 | |||
16 | @FunctionalInterface | ||
17 | interface Factory<T> { | ||
18 | StorageRefiner create(Symbol<T> symbol, Model model); | ||
19 | } | ||
20 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java index d58d026f..e59c8af8 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java | |||
@@ -15,11 +15,6 @@ public record PartialFunction<A, C>(String name, int arity, AbstractDomain<A, C> | |||
15 | } | 15 | } |
16 | 16 | ||
17 | @Override | 17 | @Override |
18 | public C defaultConcreteValue() { | ||
19 | return null; | ||
20 | } | ||
21 | |||
22 | @Override | ||
23 | public boolean equals(Object o) { | 18 | public boolean equals(Object o) { |
24 | return this == o; | 19 | return this == o; |
25 | } | 20 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java index 6b2f050b..4ccb7033 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java | |||
@@ -26,11 +26,6 @@ public record PartialRelation(String name, int arity) implements PartialSymbol<T | |||
26 | } | 26 | } |
27 | 27 | ||
28 | @Override | 28 | @Override |
29 | public Boolean defaultConcreteValue() { | ||
30 | return false; | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public List<Parameter> getParameters() { | 29 | public List<Parameter> getParameters() { |
35 | var parameters = new Parameter[arity]; | 30 | var parameters = new Parameter[arity]; |
36 | Arrays.fill(parameters, Parameter.NODE_OUT); | 31 | Arrays.fill(parameters, Parameter.NODE_OUT); |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java index 2f04534a..38b2e466 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java | |||
@@ -13,8 +13,6 @@ public sealed interface PartialSymbol<A, C> extends AnyPartialSymbol permits Par | |||
13 | 13 | ||
14 | A defaultValue(); | 14 | A defaultValue(); |
15 | 15 | ||
16 | C defaultConcreteValue(); | ||
17 | |||
18 | static PartialRelation of(String name, int arity) { | 16 | static PartialRelation of(String name, int arity) { |
19 | return new PartialRelation(name, arity); | 17 | return new PartialRelation(name, arity); |
20 | } | 18 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java new file mode 100644 index 00000000..b5a3d844 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java | |||
@@ -0,0 +1,117 @@ | |||
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.seed; | ||
7 | |||
8 | import tools.refinery.store.map.Cursor; | ||
9 | import tools.refinery.store.map.Cursors; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | import java.util.Map; | ||
13 | import java.util.Objects; | ||
14 | |||
15 | record MapBasedSeed<T>(int arity, Class<T> valueType, T reducedValue, Map<Tuple, T> map) implements Seed<T> { | ||
16 | @Override | ||
17 | public T get(Tuple key) { | ||
18 | var value = map.get(key); | ||
19 | return value == null ? reducedValue : value; | ||
20 | } | ||
21 | |||
22 | @Override | ||
23 | public Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount) { | ||
24 | if (Objects.equals(defaultValue, reducedValue)) { | ||
25 | return Cursors.of(map); | ||
26 | } | ||
27 | return new CartesianProductCursor<>(arity, nodeCount, reducedValue, defaultValue, map); | ||
28 | } | ||
29 | |||
30 | private static class CartesianProductCursor<T> implements Cursor<Tuple, T> { | ||
31 | private final int nodeCount; | ||
32 | private final T reducedValue; | ||
33 | private final T defaultValue; | ||
34 | private final Map<Tuple, T> map; | ||
35 | private final int[] counter; | ||
36 | private State state = State.INITIAL; | ||
37 | private Tuple key; | ||
38 | private T value; | ||
39 | |||
40 | private CartesianProductCursor(int arity, int nodeCount, T reducedValue, T defaultValue, Map<Tuple, T> map) { | ||
41 | this.nodeCount = nodeCount; | ||
42 | this.reducedValue = reducedValue; | ||
43 | this.defaultValue = defaultValue; | ||
44 | this.map = map; | ||
45 | counter = new int[arity]; | ||
46 | } | ||
47 | |||
48 | @Override | ||
49 | public Tuple getKey() { | ||
50 | return key; | ||
51 | } | ||
52 | |||
53 | @Override | ||
54 | public T getValue() { | ||
55 | return value; | ||
56 | } | ||
57 | |||
58 | @Override | ||
59 | public boolean isTerminated() { | ||
60 | return state == State.TERMINATED; | ||
61 | } | ||
62 | |||
63 | @Override | ||
64 | public boolean move() { | ||
65 | return switch (state) { | ||
66 | case INITIAL -> { | ||
67 | state = State.STARTED; | ||
68 | yield checkValue() || moveToNext(); | ||
69 | } | ||
70 | case STARTED -> moveToNext(); | ||
71 | case TERMINATED -> false; | ||
72 | }; | ||
73 | } | ||
74 | |||
75 | private boolean moveToNext() { | ||
76 | do { | ||
77 | increment(); | ||
78 | } while (!checkValue()); | ||
79 | return state != State.TERMINATED; | ||
80 | } | ||
81 | |||
82 | private void increment() { | ||
83 | int i = counter.length - 1; | ||
84 | while (i >= 0) { | ||
85 | counter[i]++; | ||
86 | if (counter[i] < nodeCount) { | ||
87 | return; | ||
88 | } | ||
89 | counter[i] = 0; | ||
90 | i--; | ||
91 | } | ||
92 | } | ||
93 | |||
94 | private boolean checkValue() { | ||
95 | if (state == State.TERMINATED) { | ||
96 | return false; | ||
97 | } | ||
98 | if (counter[0] >= nodeCount) { | ||
99 | state = State.TERMINATED; | ||
100 | return false; | ||
101 | } | ||
102 | key = Tuple.of(counter); | ||
103 | var valueInMap = map.get(key); | ||
104 | if (Objects.equals(valueInMap, defaultValue)) { | ||
105 | return false; | ||
106 | } | ||
107 | value = valueInMap == null ? reducedValue : valueInMap; | ||
108 | return true; | ||
109 | } | ||
110 | |||
111 | private enum State { | ||
112 | INITIAL, | ||
113 | STARTED, | ||
114 | TERMINATED | ||
115 | } | ||
116 | } | ||
117 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java index 08079f12..64b98683 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java | |||
@@ -6,14 +6,68 @@ | |||
6 | package tools.refinery.store.reasoning.seed; | 6 | package tools.refinery.store.reasoning.seed; |
7 | 7 | ||
8 | import tools.refinery.store.map.Cursor; | 8 | import tools.refinery.store.map.Cursor; |
9 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
10 | import tools.refinery.store.representation.Symbol; | ||
9 | import tools.refinery.store.tuple.Tuple; | 11 | import tools.refinery.store.tuple.Tuple; |
10 | 12 | ||
13 | import java.util.Collections; | ||
14 | import java.util.LinkedHashMap; | ||
15 | import java.util.Map; | ||
16 | |||
11 | public interface Seed<T> { | 17 | public interface Seed<T> { |
12 | int arity(); | 18 | int arity(); |
13 | 19 | ||
20 | Class<T> valueType(); | ||
21 | |||
14 | T reducedValue(); | 22 | T reducedValue(); |
15 | 23 | ||
16 | T get(Tuple key); | 24 | T get(Tuple key); |
17 | 25 | ||
18 | Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount); | 26 | Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount); |
27 | |||
28 | static <T> Builder<T> builder(int arity, Class<T> valueType, T reducedValue) { | ||
29 | return new Builder<>(arity, valueType, reducedValue); | ||
30 | } | ||
31 | |||
32 | static <T> Builder<T> builder(Symbol<T> symbol) { | ||
33 | return builder(symbol.arity(), symbol.valueType(), symbol.defaultValue()); | ||
34 | } | ||
35 | |||
36 | static <T> Builder<T> builder(PartialSymbol<T, ?> partialSymbol) { | ||
37 | return builder(partialSymbol.arity(), partialSymbol.abstractDomain().abstractType(), | ||
38 | partialSymbol.defaultValue()); | ||
39 | } | ||
40 | |||
41 | @SuppressWarnings("UnusedReturnValue") | ||
42 | class Builder<T> { | ||
43 | private final int arity; | ||
44 | private final Class<T> valueType; | ||
45 | private final T reducedValue; | ||
46 | private final Map<Tuple, T> map = new LinkedHashMap<>(); | ||
47 | |||
48 | private Builder(int arity, Class<T> valueType, T reducedValue) { | ||
49 | this.arity = arity; | ||
50 | this.valueType = valueType; | ||
51 | this.reducedValue = reducedValue; | ||
52 | } | ||
53 | |||
54 | public Builder<T> put(Tuple key, T value) { | ||
55 | if (key.getSize() != arity) { | ||
56 | throw new IllegalArgumentException("Expected %s to have %d elements".formatted(key, arity)); | ||
57 | } | ||
58 | map.put(key, value); | ||
59 | return this; | ||
60 | } | ||
61 | |||
62 | public Builder<T> putAll(Map<Tuple, T> map) { | ||
63 | for (var entry : map.entrySet()) { | ||
64 | put(entry.getKey(), entry.getValue()); | ||
65 | } | ||
66 | return this; | ||
67 | } | ||
68 | |||
69 | public Seed<T> build() { | ||
70 | return new MapBasedSeed<>(arity, valueType, reducedValue, Collections.unmodifiableMap(map)); | ||
71 | } | ||
72 | } | ||
19 | } | 73 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java new file mode 100644 index 00000000..884d6515 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java | |||
@@ -0,0 +1,27 @@ | |||
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.seed; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | ||
10 | import tools.refinery.store.representation.Symbol; | ||
11 | |||
12 | public class SeedInitializer<T> implements PartialModelInitializer { | ||
13 | private final Symbol<T> symbol; | ||
14 | private final Seed<T> seed; | ||
15 | |||
16 | public SeedInitializer(Symbol<T> symbol, Seed<T> seed) { | ||
17 | this.symbol = symbol; | ||
18 | this.seed = seed; | ||
19 | } | ||
20 | |||
21 | @Override | ||
22 | public void initialize(Model model, int nodeCount) { | ||
23 | var interpretation = model.getInterpretation(symbol); | ||
24 | var cursor = seed.getCursor(symbol.defaultValue(), nodeCount); | ||
25 | interpretation.putAll(cursor); | ||
26 | } | ||
27 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java deleted file mode 100644 index 451d1513..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/UniformSeed.java +++ /dev/null | |||
@@ -1,27 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.seed; | ||
7 | |||
8 | import tools.refinery.store.map.Cursor; | ||
9 | import tools.refinery.store.tuple.Tuple; | ||
10 | |||
11 | public record UniformSeed<T>(int arity, T reducedValue) implements Seed<T> { | ||
12 | public UniformSeed { | ||
13 | if (arity < 0) { | ||
14 | throw new IllegalArgumentException("Arity must not be negative"); | ||
15 | } | ||
16 | } | ||
17 | |||
18 | @Override | ||
19 | public T get(Tuple key) { | ||
20 | return reducedValue; | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount) { | ||
25 | return null; | ||
26 | } | ||
27 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java deleted file mode 100644 index d6a9e02c..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java +++ /dev/null | |||
@@ -1,159 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator; | ||
7 | |||
8 | import tools.refinery.store.query.substitution.Substitution; | ||
9 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
10 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
11 | import tools.refinery.store.query.term.Variable; | ||
12 | import tools.refinery.store.query.literal.Literal; | ||
13 | |||
14 | import java.util.*; | ||
15 | |||
16 | public final class Advice { | ||
17 | private final AnyPartialSymbol source; | ||
18 | private final PartialRelation target; | ||
19 | private final AdviceSlot slot; | ||
20 | private final boolean mandatory; | ||
21 | private final List<Variable> parameters; | ||
22 | private final List<Literal> literals; | ||
23 | private boolean processed; | ||
24 | |||
25 | public Advice(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot, boolean mandatory, List<Variable> parameters, List<Literal> literals) { | ||
26 | if (mandatory && !slot.isMonotonic()) { | ||
27 | throw new IllegalArgumentException("Only monotonic advice can be mandatory"); | ||
28 | } | ||
29 | this.source = source; | ||
30 | this.target = target; | ||
31 | this.slot = slot; | ||
32 | this.mandatory = mandatory; | ||
33 | checkArity(parameters); | ||
34 | this.parameters = parameters; | ||
35 | this.literals = literals; | ||
36 | } | ||
37 | |||
38 | public AnyPartialSymbol source() { | ||
39 | return source; | ||
40 | } | ||
41 | |||
42 | public PartialRelation target() { | ||
43 | return target; | ||
44 | } | ||
45 | |||
46 | public AdviceSlot slot() { | ||
47 | return slot; | ||
48 | } | ||
49 | |||
50 | public boolean mandatory() { | ||
51 | return mandatory; | ||
52 | } | ||
53 | |||
54 | public List<Variable> parameters() { | ||
55 | return parameters; | ||
56 | } | ||
57 | |||
58 | public List<Literal> literals() { | ||
59 | return literals; | ||
60 | } | ||
61 | |||
62 | public boolean processed() { | ||
63 | return processed; | ||
64 | } | ||
65 | |||
66 | public List<Literal> substitute(List<Variable> substituteParameters) { | ||
67 | checkArity(substituteParameters); | ||
68 | markProcessed(); | ||
69 | // Use a renewing substitution to remove any non-parameter variables and avoid clashed between variables | ||
70 | // coming from different advice in the same clause. | ||
71 | var substitution = Substitution.builder().putManyChecked(parameters, substituteParameters).renewing().build(); | ||
72 | return literals.stream().map(literal -> literal.substitute(substitution)).toList(); | ||
73 | } | ||
74 | |||
75 | private void markProcessed() { | ||
76 | processed = true; | ||
77 | } | ||
78 | |||
79 | public void checkProcessed() { | ||
80 | if (mandatory && !processed) { | ||
81 | throw new IllegalStateException("Mandatory advice %s was not processed".formatted(this)); | ||
82 | } | ||
83 | } | ||
84 | |||
85 | private void checkArity(List<Variable> toCheck) { | ||
86 | if (toCheck.size() != target.arity()) { | ||
87 | throw new IllegalArgumentException("%s needs %d parameters, but got %s".formatted(target.name(), | ||
88 | target.arity(), parameters.size())); | ||
89 | } | ||
90 | } | ||
91 | |||
92 | public static Builder builderFor(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) { | ||
93 | return new Builder(source, target, slot); | ||
94 | } | ||
95 | |||
96 | |||
97 | @Override | ||
98 | public String toString() { | ||
99 | return "Advice[source=%s, target=%s, slot=%s, mandatory=%s, parameters=%s, literals=%s]".formatted(source, | ||
100 | target, slot, mandatory, parameters, literals); | ||
101 | } | ||
102 | |||
103 | public static class Builder { | ||
104 | private final AnyPartialSymbol source; | ||
105 | private final PartialRelation target; | ||
106 | private final AdviceSlot slot; | ||
107 | private boolean mandatory; | ||
108 | private final List<Variable> parameters = new ArrayList<>(); | ||
109 | private final List<Literal> literals = new ArrayList<>(); | ||
110 | |||
111 | private Builder(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) { | ||
112 | this.source = source; | ||
113 | this.target = target; | ||
114 | this.slot = slot; | ||
115 | } | ||
116 | |||
117 | public Builder mandatory(boolean mandatory) { | ||
118 | this.mandatory = mandatory; | ||
119 | return this; | ||
120 | } | ||
121 | |||
122 | public Builder mandatory() { | ||
123 | return mandatory(false); | ||
124 | } | ||
125 | |||
126 | public Builder parameters(List<Variable> variables) { | ||
127 | parameters.addAll(variables); | ||
128 | return this; | ||
129 | } | ||
130 | |||
131 | public Builder parameters(Variable... variables) { | ||
132 | return parameters(List.of(variables)); | ||
133 | } | ||
134 | |||
135 | public Builder parameter(Variable variable) { | ||
136 | parameters.add(variable); | ||
137 | return this; | ||
138 | } | ||
139 | |||
140 | public Builder literals(Collection<Literal> literals) { | ||
141 | this.literals.addAll(literals); | ||
142 | return this; | ||
143 | } | ||
144 | |||
145 | public Builder literals(Literal... literals) { | ||
146 | return literals(List.of(literals)); | ||
147 | } | ||
148 | |||
149 | public Builder literal(Literal literal) { | ||
150 | literals.add(literal); | ||
151 | return this; | ||
152 | } | ||
153 | |||
154 | public Advice build() { | ||
155 | return new Advice(source, target, slot, mandatory, Collections.unmodifiableList(parameters), | ||
156 | Collections.unmodifiableList(literals)); | ||
157 | } | ||
158 | } | ||
159 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java deleted file mode 100644 index bab20340..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java +++ /dev/null | |||
@@ -1,30 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator; | ||
7 | |||
8 | import tools.refinery.store.representation.TruthValue; | ||
9 | |||
10 | public enum AdviceSlot { | ||
11 | EXTEND_MUST(true), | ||
12 | |||
13 | RESTRICT_MAY(true), | ||
14 | |||
15 | /** | ||
16 | * Same as {@link #RESTRICT_MAY}, but only active if the value of the relation is not {@link TruthValue#TRUE} or | ||
17 | * {@link TruthValue#ERROR}. | ||
18 | */ | ||
19 | RESTRICT_NEW(false); | ||
20 | |||
21 | private final boolean monotonic; | ||
22 | |||
23 | AdviceSlot(boolean monotonic) { | ||
24 | this.monotonic = monotonic; | ||
25 | } | ||
26 | |||
27 | public boolean isMonotonic() { | ||
28 | return monotonic; | ||
29 | } | ||
30 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AnyPartialSymbolTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AnyPartialSymbolTranslator.java new file mode 100644 index 00000000..48c84348 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AnyPartialSymbolTranslator.java | |||
@@ -0,0 +1,16 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
10 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
11 | |||
12 | public sealed interface AnyPartialSymbolTranslator extends ModelStoreConfiguration permits PartialSymbolTranslator { | ||
13 | AnyPartialSymbol getPartialSymbol(); | ||
14 | |||
15 | void configure(ModelStoreBuilder storeBuilder); | ||
16 | } | ||
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 new file mode 100644 index 00000000..fe8e8d6c --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java | |||
@@ -0,0 +1,263 @@ | |||
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; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.query.Constraint; | ||
10 | import tools.refinery.store.query.ModelQueryBuilder; | ||
11 | import tools.refinery.store.query.dnf.Query; | ||
12 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
13 | import tools.refinery.store.query.term.Variable; | ||
14 | import tools.refinery.store.query.view.MayView; | ||
15 | import tools.refinery.store.query.view.MustView; | ||
16 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
17 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | ||
18 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; | ||
19 | import tools.refinery.store.reasoning.interpretation.QueryBasedRelationInterpretationFactory; | ||
20 | import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter; | ||
21 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
22 | import tools.refinery.store.reasoning.literal.Modality; | ||
23 | import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner; | ||
24 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
25 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | ||
26 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
27 | import tools.refinery.store.representation.AnySymbol; | ||
28 | import tools.refinery.store.representation.Symbol; | ||
29 | import tools.refinery.store.representation.TruthValue; | ||
30 | |||
31 | @SuppressWarnings("UnusedReturnValue") | ||
32 | public final class PartialRelationTranslator extends PartialSymbolTranslator<TruthValue, Boolean> { | ||
33 | private final PartialRelation partialRelation; | ||
34 | private PartialRelationRewriter rewriter; | ||
35 | private Query<Boolean> query; | ||
36 | private Query<Boolean> may; | ||
37 | private Query<Boolean> must; | ||
38 | private Query<Boolean> candidateMay; | ||
39 | private Query<Boolean> candidateMust; | ||
40 | private RoundingMode roundingMode; | ||
41 | |||
42 | private PartialRelationTranslator(PartialRelation partialRelation) { | ||
43 | super(partialRelation); | ||
44 | this.partialRelation = partialRelation; | ||
45 | } | ||
46 | |||
47 | public PartialRelation getPartialRelation() { | ||
48 | return partialRelation; | ||
49 | } | ||
50 | |||
51 | @Override | ||
52 | public PartialRelationTranslator symbol(AnySymbol storageSymbol) { | ||
53 | super.symbol(storageSymbol); | ||
54 | return this; | ||
55 | } | ||
56 | |||
57 | @Override | ||
58 | public <T> PartialRelationTranslator symbol(Symbol<T> storageSymbol, | ||
59 | StorageRefiner.Factory<T> storageRefiner) { | ||
60 | super.symbol(storageSymbol, storageRefiner); | ||
61 | return this; | ||
62 | } | ||
63 | |||
64 | @Override | ||
65 | public PartialRelationTranslator interpretation( | ||
66 | PartialInterpretation.Factory<TruthValue, Boolean> interpretationFactory) { | ||
67 | super.interpretation(interpretationFactory); | ||
68 | return this; | ||
69 | } | ||
70 | |||
71 | @Override | ||
72 | public PartialRelationTranslator refiner( | ||
73 | PartialInterpretationRefiner.Factory<TruthValue, Boolean> interpretationRefiner) { | ||
74 | super.refiner(interpretationRefiner); | ||
75 | return this; | ||
76 | } | ||
77 | |||
78 | public PartialRelationTranslator rewriter(PartialRelationRewriter rewriter) { | ||
79 | checkNotConfigured(); | ||
80 | if (this.rewriter != null) { | ||
81 | throw new IllegalArgumentException("Rewriter was already set"); | ||
82 | } | ||
83 | this.rewriter = rewriter; | ||
84 | return this; | ||
85 | } | ||
86 | |||
87 | public PartialRelationTranslator query(RelationalQuery query) { | ||
88 | checkNotConfigured(); | ||
89 | if (this.query != null) { | ||
90 | throw new IllegalArgumentException("Query was already set"); | ||
91 | } | ||
92 | this.query = query; | ||
93 | return this; | ||
94 | } | ||
95 | |||
96 | public PartialRelationTranslator may(RelationalQuery may) { | ||
97 | checkNotConfigured(); | ||
98 | if (this.may != null) { | ||
99 | throw new IllegalArgumentException("May query was already set"); | ||
100 | } | ||
101 | this.may = may; | ||
102 | return this; | ||
103 | } | ||
104 | |||
105 | public PartialRelationTranslator must(RelationalQuery must) { | ||
106 | checkNotConfigured(); | ||
107 | if (this.must != null) { | ||
108 | throw new IllegalArgumentException("Must query was already set"); | ||
109 | } | ||
110 | this.must = must; | ||
111 | return this; | ||
112 | } | ||
113 | |||
114 | public PartialRelationTranslator candidate(RelationalQuery candidate) { | ||
115 | candidateMay(candidate); | ||
116 | candidateMust(candidate); | ||
117 | return this; | ||
118 | } | ||
119 | |||
120 | public PartialRelationTranslator candidateMay(RelationalQuery candidateMay) { | ||
121 | checkNotConfigured(); | ||
122 | if (this.candidateMay != null) { | ||
123 | throw new IllegalArgumentException("Candidate may query was already set"); | ||
124 | } | ||
125 | this.candidateMay = candidateMay; | ||
126 | return this; | ||
127 | } | ||
128 | |||
129 | public PartialRelationTranslator candidateMust(RelationalQuery candidateMust) { | ||
130 | checkNotConfigured(); | ||
131 | if (this.candidateMust != null) { | ||
132 | throw new IllegalArgumentException("Candidate must query was already set"); | ||
133 | } | ||
134 | this.candidateMust = candidateMust; | ||
135 | return this; | ||
136 | } | ||
137 | |||
138 | public PartialRelationTranslator roundingMode(RoundingMode roundingMode) { | ||
139 | checkNotConfigured(); | ||
140 | if (this.roundingMode != null) { | ||
141 | throw new IllegalArgumentException("Rounding mode was already set"); | ||
142 | } | ||
143 | this.roundingMode = roundingMode; | ||
144 | return this; | ||
145 | } | ||
146 | |||
147 | @Override | ||
148 | protected void doConfigure(ModelStoreBuilder storeBuilder) { | ||
149 | setFallbackRoundingMode(); | ||
150 | createFallbackQueryFromRewriter(); | ||
151 | liftQueries(storeBuilder); | ||
152 | createFallbackQueriesFromSymbol(); | ||
153 | setFallbackCandidateQueries(); | ||
154 | createFallbackRewriter(); | ||
155 | createFallbackInterpretation(storeBuilder); | ||
156 | createFallbackRefiner(); | ||
157 | super.doConfigure(storeBuilder); | ||
158 | } | ||
159 | |||
160 | private void setFallbackRoundingMode() { | ||
161 | if (roundingMode == null) { | ||
162 | roundingMode = query == null && storageSymbol != null ? RoundingMode.PREFER_FALSE : RoundingMode.NONE; | ||
163 | } | ||
164 | } | ||
165 | |||
166 | private RelationalQuery createQuery(Constraint constraint) { | ||
167 | int arity = partialRelation.arity(); | ||
168 | var queryBuilder = Query.builder(partialRelation.name()); | ||
169 | var parameters = new Variable[arity]; | ||
170 | for (int i = 0; i < arity; i++) { | ||
171 | parameters[i] = queryBuilder.parameter("p" + 1); | ||
172 | } | ||
173 | queryBuilder.clause(constraint.call(parameters)); | ||
174 | return queryBuilder.build(); | ||
175 | } | ||
176 | |||
177 | private void createFallbackQueryFromRewriter() { | ||
178 | if (rewriter != null && query == null) { | ||
179 | query = createQuery(partialRelation); | ||
180 | } | ||
181 | } | ||
182 | |||
183 | private void createFallbackQueriesFromSymbol() { | ||
184 | if (storageSymbol == null || storageSymbol.valueType() != TruthValue.class) { | ||
185 | return; | ||
186 | } | ||
187 | // We checked in the guard clause that this is safe. | ||
188 | @SuppressWarnings("unchecked") | ||
189 | var typedStorageSymbol = (Symbol<TruthValue>) storageSymbol; | ||
190 | var defaultValue = typedStorageSymbol.defaultValue(); | ||
191 | if (may == null && !defaultValue.may()) { | ||
192 | may = createQuery(new MayView(typedStorageSymbol)); | ||
193 | } | ||
194 | if (must == null && !defaultValue.must()) { | ||
195 | must = createQuery(new MustView(typedStorageSymbol)); | ||
196 | } | ||
197 | } | ||
198 | |||
199 | private void liftQueries(ModelStoreBuilder storeBuilder) { | ||
200 | if (query != null) { | ||
201 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | ||
202 | if (may == null) { | ||
203 | may = reasoningBuilder.lift(Modality.MAY, Concreteness.PARTIAL, query); | ||
204 | } | ||
205 | if (must == null) { | ||
206 | must = reasoningBuilder.lift(Modality.MUST, Concreteness.PARTIAL, query); | ||
207 | } | ||
208 | if (candidateMay == null) { | ||
209 | candidateMay = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); | ||
210 | } | ||
211 | if (candidateMust == null) { | ||
212 | candidateMust = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); | ||
213 | } | ||
214 | } | ||
215 | } | ||
216 | |||
217 | private void setFallbackCandidateQueries() { | ||
218 | if (candidateMay == null) { | ||
219 | candidateMay = switch (roundingMode) { | ||
220 | case NONE, PREFER_TRUE -> may; | ||
221 | case PREFER_FALSE -> must; | ||
222 | }; | ||
223 | } | ||
224 | if (candidateMust == null) { | ||
225 | candidateMust = switch (roundingMode) { | ||
226 | case NONE, PREFER_FALSE -> must; | ||
227 | case PREFER_TRUE -> may; | ||
228 | }; | ||
229 | } | ||
230 | } | ||
231 | |||
232 | private void createFallbackRewriter() { | ||
233 | if (rewriter == null) { | ||
234 | rewriter = new QueryBasedRelationRewriter(may, must, candidateMay, candidateMust); | ||
235 | } | ||
236 | } | ||
237 | |||
238 | private void createFallbackInterpretation(ModelStoreBuilder storeBuilder) { | ||
239 | if (interpretationFactory == null) { | ||
240 | var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class); | ||
241 | interpretationFactory = new QueryBasedRelationInterpretationFactory(may, must, candidateMay, candidateMust); | ||
242 | queryBuilder.queries(may, must, candidateMay, candidateMust); | ||
243 | } | ||
244 | } | ||
245 | |||
246 | private void createFallbackRefiner() { | ||
247 | if (interpretationRefiner == null && storageSymbol != null && storageSymbol.valueType() == TruthValue.class) { | ||
248 | // We checked in the condition that this is safe. | ||
249 | @SuppressWarnings("unchecked") | ||
250 | var typedStorageSymbol = (Symbol<TruthValue>) storageSymbol; | ||
251 | interpretationRefiner = ConcreteSymbolRefiner.of(typedStorageSymbol); | ||
252 | } | ||
253 | } | ||
254 | |||
255 | public PartialRelationRewriter getRewriter() { | ||
256 | checkConfigured(); | ||
257 | return rewriter; | ||
258 | } | ||
259 | |||
260 | public static PartialRelationTranslator of(PartialRelation relation) { | ||
261 | return new PartialRelationTranslator(relation); | ||
262 | } | ||
263 | } | ||
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 new file mode 100644 index 00000000..07d1d19b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java | |||
@@ -0,0 +1,156 @@ | |||
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; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
10 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | ||
11 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
12 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | ||
13 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | ||
14 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
15 | import tools.refinery.store.reasoning.seed.Seed; | ||
16 | import tools.refinery.store.reasoning.seed.SeedInitializer; | ||
17 | import tools.refinery.store.representation.AnySymbol; | ||
18 | import tools.refinery.store.representation.Symbol; | ||
19 | |||
20 | @SuppressWarnings("UnusedReturnValue") | ||
21 | public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartialSymbolTranslator | ||
22 | permits PartialRelationTranslator { | ||
23 | private final PartialSymbol<A, C> partialSymbol; | ||
24 | private boolean configured = false; | ||
25 | protected PartialInterpretationRefiner.Factory<A, C> interpretationRefiner; | ||
26 | protected AnySymbol storageSymbol; | ||
27 | protected StorageRefiner.Factory<?> storageRefiner; | ||
28 | protected PartialInterpretation.Factory<A, C> interpretationFactory; | ||
29 | protected PartialModelInitializer initializer; | ||
30 | |||
31 | PartialSymbolTranslator(PartialSymbol<A, C> partialSymbol) { | ||
32 | this.partialSymbol = partialSymbol; | ||
33 | } | ||
34 | |||
35 | @Override | ||
36 | public PartialSymbol<A, C> getPartialSymbol() { | ||
37 | return partialSymbol; | ||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public void apply(ModelStoreBuilder storeBuilder) { | ||
42 | storeBuilder.getAdapter(ReasoningBuilder.class).partialSymbol(this); | ||
43 | } | ||
44 | |||
45 | public boolean isConfigured() { | ||
46 | return configured; | ||
47 | } | ||
48 | |||
49 | protected void checkConfigured() { | ||
50 | if (!configured) { | ||
51 | throw new IllegalStateException("Partial symbol was not configured"); | ||
52 | } | ||
53 | } | ||
54 | |||
55 | protected void checkNotConfigured() { | ||
56 | if (configured) { | ||
57 | throw new IllegalStateException("Partial symbol was already configured"); | ||
58 | } | ||
59 | } | ||
60 | |||
61 | public PartialSymbolTranslator<A, C> symbol(AnySymbol storageSymbol) { | ||
62 | return symbol((Symbol<?>) storageSymbol, null); | ||
63 | } | ||
64 | |||
65 | public <T> PartialSymbolTranslator<A, C> symbol(Symbol<T> storageSymbol, | ||
66 | StorageRefiner.Factory<T> storageRefiner) { | ||
67 | checkNotConfigured(); | ||
68 | if (this.storageSymbol != null) { | ||
69 | throw new IllegalStateException("Representation symbol was already set"); | ||
70 | } | ||
71 | this.storageSymbol = storageSymbol; | ||
72 | this.storageRefiner = storageRefiner; | ||
73 | return this; | ||
74 | } | ||
75 | |||
76 | public PartialSymbolTranslator<A, C> interpretation(PartialInterpretation.Factory<A, C> interpretationFactory) { | ||
77 | checkNotConfigured(); | ||
78 | if (this.interpretationFactory != null) { | ||
79 | throw new IllegalStateException("Interpretation factory was already set"); | ||
80 | } | ||
81 | this.interpretationFactory = interpretationFactory; | ||
82 | return this; | ||
83 | } | ||
84 | |||
85 | public PartialSymbolTranslator<A, C> refiner(PartialInterpretationRefiner.Factory<A, C> interpretationRefiner) { | ||
86 | checkNotConfigured(); | ||
87 | if (this.interpretationRefiner != null) { | ||
88 | throw new IllegalStateException("Interpretation refiner was already set"); | ||
89 | } | ||
90 | this.interpretationRefiner = interpretationRefiner; | ||
91 | return this; | ||
92 | } | ||
93 | |||
94 | public PartialSymbolTranslator<A, C> initializer(PartialModelInitializer initializer) { | ||
95 | checkNotConfigured(); | ||
96 | if (this.initializer != null) { | ||
97 | throw new IllegalStateException("Initializer was already set"); | ||
98 | } | ||
99 | this.initializer = initializer; | ||
100 | return this; | ||
101 | } | ||
102 | |||
103 | public <T> PartialSymbolTranslator<A, C> seed(Seed<T> seed) { | ||
104 | if (storageSymbol == null) { | ||
105 | throw new IllegalArgumentException("Seed requires setting a storage symbol"); | ||
106 | } | ||
107 | if (!seed.valueType().equals(storageSymbol.valueType())) { | ||
108 | throw new IllegalArgumentException("Seed type %s does not match storage symbol type %s" | ||
109 | .formatted(seed.valueType(), storageSymbol.valueType())); | ||
110 | } | ||
111 | // The guard clause only allows a well-typed seed. | ||
112 | @SuppressWarnings("unchecked") | ||
113 | var typedStorageSymbol = (Symbol<T>) storageSymbol; | ||
114 | return initializer(new SeedInitializer<>(typedStorageSymbol, seed)); | ||
115 | } | ||
116 | |||
117 | @Override | ||
118 | public void configure(ModelStoreBuilder storeBuilder) { | ||
119 | checkNotConfigured(); | ||
120 | doConfigure(storeBuilder); | ||
121 | configured = true; | ||
122 | } | ||
123 | |||
124 | protected void doConfigure(ModelStoreBuilder storeBuilder) { | ||
125 | if (interpretationFactory == null) { | ||
126 | throw new IllegalArgumentException("Interpretation factory must be set"); | ||
127 | } | ||
128 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | ||
129 | if (storageSymbol != null) { | ||
130 | storeBuilder.symbol(storageSymbol); | ||
131 | if (storageRefiner != null) { | ||
132 | registerStorageRefiner(reasoningBuilder, storageRefiner); | ||
133 | } | ||
134 | } | ||
135 | if (initializer != null) { | ||
136 | reasoningBuilder.initializer(initializer); | ||
137 | } | ||
138 | } | ||
139 | |||
140 | private <T> void registerStorageRefiner(ReasoningBuilder reasoningBuilder, StorageRefiner.Factory<T> factory) { | ||
141 | // The builder only allows setting a well-typed representation refiner. | ||
142 | @SuppressWarnings("unchecked") | ||
143 | var typedStorageSymbol = (Symbol<T>) storageSymbol; | ||
144 | reasoningBuilder.storageRefiner(typedStorageSymbol, factory); | ||
145 | } | ||
146 | |||
147 | public PartialInterpretation.Factory<A, C> getInterpretationFactory() { | ||
148 | checkConfigured(); | ||
149 | return interpretationFactory; | ||
150 | } | ||
151 | |||
152 | public PartialInterpretationRefiner.Factory<A, C> getInterpretationRefiner() { | ||
153 | checkConfigured(); | ||
154 | return interpretationRefiner; | ||
155 | } | ||
156 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/RoundingMode.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/RoundingMode.java new file mode 100644 index 00000000..dd956a50 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/RoundingMode.java | |||
@@ -0,0 +1,12 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator; | ||
7 | |||
8 | public enum RoundingMode { | ||
9 | NONE, | ||
10 | PREFER_TRUE, | ||
11 | PREFER_FALSE | ||
12 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java deleted file mode 100644 index 4a5a8843..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslatedRelation.java +++ /dev/null | |||
@@ -1,27 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.query.term.Variable; | ||
10 | import tools.refinery.store.query.literal.CallPolarity; | ||
11 | import tools.refinery.store.query.literal.Literal; | ||
12 | import tools.refinery.store.reasoning.PartialInterpretation; | ||
13 | import tools.refinery.store.reasoning.literal.Modality; | ||
14 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
15 | import tools.refinery.store.representation.TruthValue; | ||
16 | |||
17 | import java.util.List; | ||
18 | |||
19 | public interface TranslatedRelation { | ||
20 | PartialRelation getSource(); | ||
21 | |||
22 | void configure(List<Advice> advices); | ||
23 | |||
24 | List<Literal> call(CallPolarity polarity, Modality modality, List<Variable> arguments); | ||
25 | |||
26 | PartialInterpretation<TruthValue, Boolean> createPartialInterpretation(Model model); | ||
27 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java deleted file mode 100644 index 6e44a7d7..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java +++ /dev/null | |||
@@ -1,32 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
10 | |||
11 | import java.util.Collection; | ||
12 | |||
13 | public abstract class TranslationUnit { | ||
14 | private ReasoningBuilder reasoningBuilder; | ||
15 | |||
16 | protected ReasoningBuilder getReasoningBuilder() { | ||
17 | return reasoningBuilder; | ||
18 | } | ||
19 | |||
20 | public void setPartialInterpretationBuilder(ReasoningBuilder reasoningBuilder) { | ||
21 | this.reasoningBuilder = reasoningBuilder; | ||
22 | configureReasoningBuilder(); | ||
23 | } | ||
24 | |||
25 | protected void configureReasoningBuilder() { | ||
26 | // Nothing to configure by default. | ||
27 | } | ||
28 | |||
29 | public abstract Collection<TranslatedRelation> getTranslatedRelations(); | ||
30 | |||
31 | public abstract void initializeModel(Model model, int nodeCount); | ||
32 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java deleted file mode 100644 index 2a151aa2..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionInterpretation.java +++ /dev/null | |||
@@ -1,93 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.base; | ||
7 | |||
8 | import tools.refinery.store.map.Cursor; | ||
9 | import tools.refinery.store.model.Interpretation; | ||
10 | import tools.refinery.store.query.resultset.ResultSet; | ||
11 | import tools.refinery.store.reasoning.MergeResult; | ||
12 | import tools.refinery.store.reasoning.PartialInterpretation; | ||
13 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
14 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
15 | import tools.refinery.store.representation.TruthValue; | ||
16 | import tools.refinery.store.tuple.Tuple; | ||
17 | |||
18 | public class BaseDecisionInterpretation implements PartialInterpretation<TruthValue, Boolean> { | ||
19 | private final ReasoningAdapter reasoningAdapter; | ||
20 | private PartialRelation partialRelation; | ||
21 | private final ResultSet<Boolean> mustResultSet; | ||
22 | private final ResultSet<Boolean> mayResultSet; | ||
23 | private final ResultSet<Boolean> errorResultSet; | ||
24 | private final ResultSet<Boolean> currentResultSet; | ||
25 | private final Interpretation<TruthValue> interpretation; | ||
26 | |||
27 | public BaseDecisionInterpretation(ReasoningAdapter reasoningAdapter, ResultSet<Boolean> mustResultSet, | ||
28 | ResultSet<Boolean> mayResultSet, ResultSet<Boolean> errorResultSet, | ||
29 | ResultSet<Boolean> currentResultSet, Interpretation<TruthValue> interpretation) { | ||
30 | this.reasoningAdapter = reasoningAdapter; | ||
31 | this.mustResultSet = mustResultSet; | ||
32 | this.mayResultSet = mayResultSet; | ||
33 | this.errorResultSet = errorResultSet; | ||
34 | this.currentResultSet = currentResultSet; | ||
35 | this.interpretation = interpretation; | ||
36 | } | ||
37 | |||
38 | @Override | ||
39 | public ReasoningAdapter getAdapter() { | ||
40 | return reasoningAdapter; | ||
41 | } | ||
42 | |||
43 | @Override | ||
44 | public int countUnfinished() { | ||
45 | return 0; | ||
46 | } | ||
47 | |||
48 | @Override | ||
49 | public int countErrors() { | ||
50 | return errorResultSet.size(); | ||
51 | } | ||
52 | |||
53 | @Override | ||
54 | public PartialRelation getPartialSymbol() { | ||
55 | return partialRelation; | ||
56 | } | ||
57 | |||
58 | @Override | ||
59 | public TruthValue get(Tuple key) { | ||
60 | return null; | ||
61 | } | ||
62 | |||
63 | @Override | ||
64 | public Cursor<Tuple, TruthValue> getAll() { | ||
65 | return null; | ||
66 | } | ||
67 | |||
68 | @Override | ||
69 | public MergeResult merge(Tuple key, TruthValue value) { | ||
70 | TruthValue newValue; | ||
71 | switch (value) { | ||
72 | case UNKNOWN -> { | ||
73 | return MergeResult.UNCHANGED; | ||
74 | } | ||
75 | case TRUE -> newValue = mayResultSet.get(key) ? TruthValue.TRUE : TruthValue.ERROR; | ||
76 | case FALSE -> newValue = mustResultSet.get(key) ? TruthValue.ERROR : TruthValue.FALSE; | ||
77 | case ERROR -> newValue = TruthValue.ERROR; | ||
78 | default -> throw new IllegalArgumentException("Unknown truth value: " + value); | ||
79 | } | ||
80 | var oldValue = interpretation.put(key, newValue); | ||
81 | return oldValue == TruthValue.ERROR ? MergeResult.UNCHANGED : MergeResult.REFINED; | ||
82 | } | ||
83 | |||
84 | @Override | ||
85 | public Boolean getConcrete(Tuple key) { | ||
86 | return currentResultSet.get(key); | ||
87 | } | ||
88 | |||
89 | @Override | ||
90 | public Cursor<Tuple, Boolean> getAllConcrete() { | ||
91 | return null; | ||
92 | } | ||
93 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java deleted file mode 100644 index a1e4b816..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/BaseDecisionTranslationUnit.java +++ /dev/null | |||
@@ -1,49 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.base; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
10 | import tools.refinery.store.reasoning.seed.Seed; | ||
11 | import tools.refinery.store.reasoning.seed.UniformSeed; | ||
12 | import tools.refinery.store.reasoning.translator.TranslatedRelation; | ||
13 | import tools.refinery.store.reasoning.translator.TranslationUnit; | ||
14 | import tools.refinery.store.representation.Symbol; | ||
15 | import tools.refinery.store.representation.TruthValue; | ||
16 | |||
17 | import java.util.Collection; | ||
18 | import java.util.List; | ||
19 | |||
20 | public class BaseDecisionTranslationUnit extends TranslationUnit { | ||
21 | private final PartialRelation partialRelation; | ||
22 | private final Seed<TruthValue> seed; | ||
23 | private final Symbol<TruthValue> symbol; | ||
24 | |||
25 | public BaseDecisionTranslationUnit(PartialRelation partialRelation, Seed<TruthValue> seed) { | ||
26 | if (seed.arity() != partialRelation.arity()) { | ||
27 | throw new IllegalArgumentException("Expected seed with arity %d for %s, got arity %s" | ||
28 | .formatted(partialRelation.arity(), partialRelation, seed.arity())); | ||
29 | } | ||
30 | this.partialRelation = partialRelation; | ||
31 | this.seed = seed; | ||
32 | symbol = Symbol.of(partialRelation.name(), partialRelation.arity(), TruthValue.class, TruthValue.UNKNOWN); | ||
33 | } | ||
34 | |||
35 | public BaseDecisionTranslationUnit(PartialRelation partialRelation) { | ||
36 | this(partialRelation, new UniformSeed<>(partialRelation.arity(), TruthValue.UNKNOWN)); | ||
37 | } | ||
38 | |||
39 | @Override | ||
40 | public Collection<TranslatedRelation> getTranslatedRelations() { | ||
41 | return List.of(new TranslatedBaseDecision(getReasoningBuilder(), partialRelation, symbol)); | ||
42 | } | ||
43 | |||
44 | @Override | ||
45 | public void initializeModel(Model model, int nodeCount) { | ||
46 | var interpretation = model.getInterpretation(symbol); | ||
47 | interpretation.putAll(seed.getCursor(TruthValue.UNKNOWN, nodeCount)); | ||
48 | } | ||
49 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java deleted file mode 100644 index 4782eb46..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/base/TranslatedBaseDecision.java +++ /dev/null | |||
@@ -1,54 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.base; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.query.term.Variable; | ||
10 | import tools.refinery.store.query.literal.CallPolarity; | ||
11 | import tools.refinery.store.query.literal.Literal; | ||
12 | import tools.refinery.store.reasoning.PartialInterpretation; | ||
13 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
14 | import tools.refinery.store.reasoning.literal.Modality; | ||
15 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
16 | import tools.refinery.store.reasoning.translator.Advice; | ||
17 | import tools.refinery.store.reasoning.translator.TranslatedRelation; | ||
18 | import tools.refinery.store.representation.Symbol; | ||
19 | import tools.refinery.store.representation.TruthValue; | ||
20 | |||
21 | import java.util.List; | ||
22 | |||
23 | class TranslatedBaseDecision implements TranslatedRelation { | ||
24 | private final ReasoningBuilder reasoningBuilder; | ||
25 | private final PartialRelation partialRelation; | ||
26 | private final Symbol<TruthValue> symbol; | ||
27 | |||
28 | public TranslatedBaseDecision(ReasoningBuilder reasoningBuilder, PartialRelation partialRelation, | ||
29 | Symbol<TruthValue> symbol) { | ||
30 | this.reasoningBuilder = reasoningBuilder; | ||
31 | this.partialRelation = partialRelation; | ||
32 | this.symbol = symbol; | ||
33 | } | ||
34 | |||
35 | @Override | ||
36 | public PartialRelation getSource() { | ||
37 | return partialRelation; | ||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public void configure(List<Advice> advices) { | ||
42 | |||
43 | } | ||
44 | |||
45 | @Override | ||
46 | public List<Literal> call(CallPolarity polarity, Modality modality, List<Variable> arguments) { | ||
47 | return null; | ||
48 | } | ||
49 | |||
50 | @Override | ||
51 | public PartialInterpretation<TruthValue, Boolean> createPartialInterpretation(Model model) { | ||
52 | return null; | ||
53 | } | ||
54 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeView.java deleted file mode 100644 index 40de4644..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeView.java +++ /dev/null | |||
@@ -1,40 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.query.view.TuplePreservingView; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | import java.util.Objects; | ||
13 | |||
14 | class InferredMayTypeView extends TuplePreservingView<InferredType> { | ||
15 | private final PartialRelation type; | ||
16 | |||
17 | InferredMayTypeView(PartialRelation type) { | ||
18 | super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#may".formatted(type)); | ||
19 | this.type = type; | ||
20 | } | ||
21 | |||
22 | @Override | ||
23 | protected boolean doFilter(Tuple key, InferredType value) { | ||
24 | return value.mayConcreteTypes().contains(type); | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public boolean equals(Object o) { | ||
29 | if (this == o) return true; | ||
30 | if (o == null || getClass() != o.getClass()) return false; | ||
31 | if (!super.equals(o)) return false; | ||
32 | InferredMayTypeView that = (InferredMayTypeView) o; | ||
33 | return Objects.equals(type, that.type); | ||
34 | } | ||
35 | |||
36 | @Override | ||
37 | public int hashCode() { | ||
38 | return Objects.hash(super.hashCode(), type); | ||
39 | } | ||
40 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeView.java deleted file mode 100644 index 1a121547..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeView.java +++ /dev/null | |||
@@ -1,40 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
9 | import tools.refinery.store.query.view.TuplePreservingView; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | import java.util.Objects; | ||
13 | |||
14 | class InferredMustTypeView extends TuplePreservingView<InferredType> { | ||
15 | private final PartialRelation type; | ||
16 | |||
17 | InferredMustTypeView(PartialRelation type) { | ||
18 | super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#must".formatted(type)); | ||
19 | this.type = type; | ||
20 | } | ||
21 | |||
22 | @Override | ||
23 | protected boolean doFilter(Tuple key, InferredType value) { | ||
24 | return value.mustTypes().contains(type); | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public boolean equals(Object o) { | ||
29 | if (this == o) return true; | ||
30 | if (o == null || getClass() != o.getClass()) return false; | ||
31 | if (!super.equals(o)) return false; | ||
32 | InferredMustTypeView that = (InferredMustTypeView) o; | ||
33 | return Objects.equals(type, that.type); | ||
34 | } | ||
35 | |||
36 | @Override | ||
37 | public int hashCode() { | ||
38 | return Objects.hash(super.hashCode(), type); | ||
39 | } | ||
40 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java deleted file mode 100644 index 06e3c05f..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java +++ /dev/null | |||
@@ -1,37 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
10 | import tools.refinery.store.reasoning.translator.TranslatedRelation; | ||
11 | import tools.refinery.store.reasoning.translator.TranslationUnit; | ||
12 | import tools.refinery.store.representation.Symbol; | ||
13 | |||
14 | import java.util.Collection; | ||
15 | import java.util.List; | ||
16 | import java.util.Map; | ||
17 | |||
18 | public class TypeHierarchyTranslationUnit extends TranslationUnit { | ||
19 | static final Symbol<InferredType> INFERRED_TYPE_SYMBOL = Symbol.of( | ||
20 | "inferredType", 1, InferredType.class, InferredType.UNTYPED); | ||
21 | |||
22 | private final TypeAnalyzer typeAnalyzer; | ||
23 | |||
24 | public TypeHierarchyTranslationUnit(Map<PartialRelation, TypeInfo> typeInfoMap) { | ||
25 | typeAnalyzer = new TypeAnalyzer(typeInfoMap); | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public Collection<TranslatedRelation> getTranslatedRelations() { | ||
30 | return List.of(); | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public void initializeModel(Model model, int nodeCount) { | ||
35 | |||
36 | } | ||
37 | } | ||
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java new file mode 100644 index 00000000..f948ad6a --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/PartialModelTest.java | |||
@@ -0,0 +1,91 @@ | |||
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; | ||
7 | |||
8 | import org.junit.jupiter.api.Test; | ||
9 | import tools.refinery.store.model.ModelStore; | ||
10 | import tools.refinery.store.query.ModelQueryAdapter; | ||
11 | import tools.refinery.store.query.dnf.Query; | ||
12 | import tools.refinery.store.query.term.Variable; | ||
13 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; | ||
14 | import tools.refinery.store.query.view.ForbiddenView; | ||
15 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
16 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
17 | import tools.refinery.store.reasoning.seed.Seed; | ||
18 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
19 | import tools.refinery.store.representation.Symbol; | ||
20 | import tools.refinery.store.representation.TruthValue; | ||
21 | import tools.refinery.store.tuple.Tuple; | ||
22 | |||
23 | import static org.hamcrest.MatcherAssert.assertThat; | ||
24 | import static org.hamcrest.Matchers.is; | ||
25 | import static tools.refinery.store.query.literal.Literals.not; | ||
26 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | ||
27 | |||
28 | class PartialModelTest { | ||
29 | @Test | ||
30 | void partialModelTest() { | ||
31 | var personStorage = Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE); | ||
32 | var friendStorage = Symbol.of("friend", 2, TruthValue.class, TruthValue.UNKNOWN); | ||
33 | |||
34 | var person = new PartialRelation("Person", 1); | ||
35 | var friend = new PartialRelation("friend", 2); | ||
36 | var lonely = new PartialRelation("lonely", 1); | ||
37 | |||
38 | var store = ModelStore.builder() | ||
39 | .with(ViatraModelQueryAdapter.builder()) | ||
40 | .with(ReasoningAdapter.builder() | ||
41 | .initialNodeCount(4)) | ||
42 | .with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL) | ||
43 | .symbol(Symbol.of("exists", 1, TruthValue.class, TruthValue.FALSE)) | ||
44 | .seed(Seed.builder(ReasoningAdapter.EXISTS_SYMBOL) | ||
45 | .put(Tuple.of(0), TruthValue.TRUE) | ||
46 | .put(Tuple.of(1), TruthValue.UNKNOWN) | ||
47 | .put(Tuple.of(2), TruthValue.TRUE) | ||
48 | .put(Tuple.of(3), TruthValue.TRUE) | ||
49 | .build())) | ||
50 | .with(PartialRelationTranslator.of(person) | ||
51 | .symbol(personStorage) | ||
52 | .seed(Seed.builder(personStorage) | ||
53 | .put(Tuple.of(0), TruthValue.TRUE) | ||
54 | .put(Tuple.of(1), TruthValue.TRUE) | ||
55 | .put(Tuple.of(2), TruthValue.UNKNOWN) | ||
56 | .build())) | ||
57 | .with(PartialRelationTranslator.of(friend) | ||
58 | .symbol(friendStorage) | ||
59 | .may(Query.of((builder, p1, p2) -> builder.clause( | ||
60 | may(person.call(p1)), | ||
61 | may(person.call(p2)), | ||
62 | // not(must(EQUALS_SYMBOL.call(p1, p2))), | ||
63 | not(new ForbiddenView(friendStorage).call(p1, p2)) | ||
64 | ))) | ||
65 | .seed(Seed.builder(friendStorage) | ||
66 | .put(Tuple.of(0, 1), TruthValue.TRUE) | ||
67 | .put(Tuple.of(1, 2), TruthValue.FALSE) | ||
68 | .build())) | ||
69 | .with(PartialRelationTranslator.of(lonely) | ||
70 | .query(Query.of((builder, p1) -> builder.clause( | ||
71 | person.call(p1), | ||
72 | not(friend.call(p1, Variable.of()))) | ||
73 | ))) | ||
74 | .build(); | ||
75 | |||
76 | var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(); | ||
77 | |||
78 | var queryAdapter = model.getAdapter(ModelQueryAdapter.class); | ||
79 | var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
80 | var friendInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, friend); | ||
81 | assertThat(friendInterpretation.get(Tuple.of(0, 1)), is(TruthValue.TRUE)); | ||
82 | assertThat(friendInterpretation.get(Tuple.of(1, 0)), is(TruthValue.UNKNOWN)); | ||
83 | assertThat(friendInterpretation.get(Tuple.of(3, 0)), is(TruthValue.FALSE)); | ||
84 | var friendRefiner = reasoningAdapter.getRefiner(friend); | ||
85 | assertThat(friendRefiner.merge(Tuple.of(0, 1), TruthValue.FALSE), is(true)); | ||
86 | assertThat(friendRefiner.merge(Tuple.of(1, 0), TruthValue.TRUE), is(true)); | ||
87 | queryAdapter.flushChanges(); | ||
88 | assertThat(friendInterpretation.get(Tuple.of(0, 1)), is(TruthValue.ERROR)); | ||
89 | assertThat(friendInterpretation.get(Tuple.of(1, 0)), is(TruthValue.TRUE)); | ||
90 | } | ||
91 | } | ||
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java index ceb9404a..793d1cec 100644 --- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/lifting/DnfLifterTest.java | |||
@@ -55,7 +55,7 @@ class DnfLifterTest { | |||
55 | 55 | ||
56 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | 56 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( |
57 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, v1), | 57 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, v1), |
58 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) | 58 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1) |
59 | ))).getDnf(); | 59 | ))).getDnf(); |
60 | 60 | ||
61 | assertThat(actual, structurallyEqualTo(expected)); | 61 | assertThat(actual, structurallyEqualTo(expected)); |
@@ -74,7 +74,7 @@ class DnfLifterTest { | |||
74 | 74 | ||
75 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | 75 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( |
76 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, called.getDnf()).call(p1, v1), | 76 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, called.getDnf()).call(p1, v1), |
77 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) | 77 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1) |
78 | ))).getDnf(); | 78 | ))).getDnf(); |
79 | 79 | ||
80 | assertThat(actual, structurallyEqualTo(expected)); | 80 | assertThat(actual, structurallyEqualTo(expected)); |
@@ -89,7 +89,7 @@ class DnfLifterTest { | |||
89 | 89 | ||
90 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | 90 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( |
91 | friendMustView.call(p1, v1), | 91 | friendMustView.call(p1, v1), |
92 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) | 92 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1) |
93 | ))).getDnf(); | 93 | ))).getDnf(); |
94 | 94 | ||
95 | assertThat(actual, structurallyEqualTo(expected)); | 95 | assertThat(actual, structurallyEqualTo(expected)); |
@@ -106,7 +106,7 @@ class DnfLifterTest { | |||
106 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | 106 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( |
107 | not(ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, v1)), | 107 | not(ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, v1)), |
108 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(v1, p1), | 108 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(v1, p1), |
109 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) | 109 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1) |
110 | ))).getDnf(); | 110 | ))).getDnf(); |
111 | 111 | ||
112 | assertThat(actual, structurallyEqualTo(expected)); | 112 | assertThat(actual, structurallyEqualTo(expected)); |
@@ -122,7 +122,7 @@ class DnfLifterTest { | |||
122 | 122 | ||
123 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( | 123 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( |
124 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, p2), | 124 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, p2), |
125 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | 125 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2) |
126 | )); | 126 | )); |
127 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | 127 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( |
128 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), | 128 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), |
@@ -142,7 +142,7 @@ class DnfLifterTest { | |||
142 | 142 | ||
143 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( | 143 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( |
144 | friendMustView.call(p1, p2), | 144 | friendMustView.call(p1, p2), |
145 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | 145 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2) |
146 | )); | 146 | )); |
147 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | 147 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( |
148 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), | 148 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), |
@@ -161,7 +161,7 @@ class DnfLifterTest { | |||
161 | 161 | ||
162 | var helper = Query.of("Helper", (builder, p1) -> builder.clause( | 162 | var helper = Query.of("Helper", (builder, p1) -> builder.clause( |
163 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, p1), | 163 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, friend).call(p1, p1), |
164 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p1) | 164 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p1) |
165 | )); | 165 | )); |
166 | var expected = Query.of("Expected", (builder) -> builder.clause((v1) -> List.of( | 166 | var expected = Query.of("Expected", (builder) -> builder.clause((v1) -> List.of( |
167 | not(helper.call(v1)) | 167 | not(helper.call(v1)) |
@@ -191,7 +191,7 @@ class DnfLifterTest { | |||
191 | var p2 = builder.parameter("p2", ParameterDirection.OUT); | 191 | var p2 = builder.parameter("p2", ParameterDirection.OUT); |
192 | builder.clause( | 192 | builder.clause( |
193 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, called).call(p1, p2), | 193 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, called).call(p1, p2), |
194 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | 194 | ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2) |
195 | ); | 195 | ); |
196 | }); | 196 | }); |
197 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | 197 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( |
@@ -212,7 +212,7 @@ class DnfLifterTest { | |||
212 | 212 | ||
213 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( | 213 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( |
214 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), | 214 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), |
215 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | 215 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2) |
216 | )); | 216 | )); |
217 | var helper2 = Query.of("Helper2", (builder, p1, p2) -> { | 217 | var helper2 = Query.of("Helper2", (builder, p1, p2) -> { |
218 | builder.clause( | 218 | builder.clause( |
@@ -241,7 +241,7 @@ class DnfLifterTest { | |||
241 | 241 | ||
242 | var endExistsHelper = Query.of("EndExistsHelper", (builder, p1, p2) -> builder.clause( | 242 | var endExistsHelper = Query.of("EndExistsHelper", (builder, p1, p2) -> builder.clause( |
243 | friendMustView.call(p1, p2), | 243 | friendMustView.call(p1, p2), |
244 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | 244 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2) |
245 | )); | 245 | )); |
246 | var transitiveHelper = Query.of("TransitiveHelper", (builder, p1, p2) -> { | 246 | var transitiveHelper = Query.of("TransitiveHelper", (builder, p1, p2) -> { |
247 | builder.clause( | 247 | builder.clause( |
@@ -270,7 +270,7 @@ class DnfLifterTest { | |||
270 | 270 | ||
271 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( | 271 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( |
272 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), | 272 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), |
273 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | 273 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2) |
274 | )); | 274 | )); |
275 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | 275 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( |
276 | helper.callTransitive(p1, v1), | 276 | helper.callTransitive(p1, v1), |
@@ -291,11 +291,11 @@ class DnfLifterTest { | |||
291 | 291 | ||
292 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( | 292 | var helper = Query.of("Helper", (builder, p1, p2) -> builder.clause( |
293 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), | 293 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), |
294 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | 294 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2) |
295 | )); | 295 | )); |
296 | var helper2 = Query.of("Helper2", (builder, p1, p2) -> builder.clause( | 296 | var helper2 = Query.of("Helper2", (builder, p1, p2) -> builder.clause( |
297 | friendMustView.call(p1, p2), | 297 | friendMustView.call(p1, p2), |
298 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(p2) | 298 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(p2) |
299 | )); | 299 | )); |
300 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | 300 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( |
301 | helper.callTransitive(p1, v1), | 301 | helper.callTransitive(p1, v1), |
@@ -316,7 +316,7 @@ class DnfLifterTest { | |||
316 | 316 | ||
317 | var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( | 317 | var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( |
318 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), | 318 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, person).call(p1), |
319 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EQUALS).call(p2, p1) | 319 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EQUALS_SYMBOL).call(p2, p1) |
320 | )).getDnf(); | 320 | )).getDnf(); |
321 | 321 | ||
322 | assertThat(actual, structurallyEqualTo(expected)); | 322 | assertThat(actual, structurallyEqualTo(expected)); |
@@ -332,7 +332,7 @@ class DnfLifterTest { | |||
332 | 332 | ||
333 | var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( | 333 | var expected = Query.of("Expected", (builder, p1, p2) -> builder.clause( |
334 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), | 334 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(p1, p2), |
335 | not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EQUALS).call(p1, p2)) | 335 | not(ModalConstraint.of(Modality.MUST, Concreteness.PARTIAL, ReasoningAdapter.EQUALS_SYMBOL).call(p1, p2)) |
336 | )).getDnf(); | 336 | )).getDnf(); |
337 | 337 | ||
338 | assertThat(actual, structurallyEqualTo(expected)); | 338 | assertThat(actual, structurallyEqualTo(expected)); |
@@ -349,7 +349,7 @@ class DnfLifterTest { | |||
349 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( | 349 | var expected = Query.of("Expected", (builder, p1) -> builder.clause((v1) -> List.of( |
350 | v1.isConstant(0), | 350 | v1.isConstant(0), |
351 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(v1, p1), | 351 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, friend).call(v1, p1), |
352 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS).call(v1) | 352 | ModalConstraint.of(Modality.MAY, Concreteness.PARTIAL, ReasoningAdapter.EXISTS_SYMBOL).call(v1) |
353 | ))).getDnf(); | 353 | ))).getDnf(); |
354 | 354 | ||
355 | assertThat(actual, structurallyEqualTo(expected)); | 355 | assertThat(actual, structurallyEqualTo(expected)); |
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java index 05a476c6..b4ba16fc 100644 --- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java | |||
@@ -5,6 +5,7 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | 6 | package tools.refinery.store.reasoning.translator.typehierarchy; |
7 | 7 | ||
8 | import org.hamcrest.Matchers; | ||
8 | import org.junit.jupiter.api.BeforeEach; | 9 | import org.junit.jupiter.api.BeforeEach; |
9 | import org.junit.jupiter.api.Test; | 10 | import org.junit.jupiter.api.Test; |
10 | import tools.refinery.store.reasoning.representation.PartialRelation; | 11 | import tools.refinery.store.reasoning.representation.PartialRelation; |
@@ -65,16 +66,16 @@ class TypeAnalyzerExampleHierarchyTest { | |||
65 | @Test | 66 | @Test |
66 | void inferredTypesTest() { | 67 | void inferredTypesTest() { |
67 | assertAll( | 68 | assertAll( |
68 | () -> assertThat(sut.getUnknownType(), is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))), | 69 | () -> assertThat(sut.getUnknownType(), Matchers.is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))), |
69 | () -> assertThat(tester.getInferredType(a1), is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))), | 70 | () -> assertThat(tester.getInferredType(a1), Matchers.is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))), |
70 | () -> assertThat(tester.getInferredType(a3), is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))), | 71 | () -> assertThat(tester.getInferredType(a3), Matchers.is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))), |
71 | () -> assertThat(tester.getInferredType(a4), is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))), | 72 | () -> assertThat(tester.getInferredType(a4), Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))), |
72 | () -> assertThat(tester.getInferredType(a5), is(new InferredType(Set.of(a5), Set.of(), null))), | 73 | () -> assertThat(tester.getInferredType(a5), Matchers.is(new InferredType(Set.of(a5), Set.of(), null))), |
73 | () -> assertThat(tester.getInferredType(c1), is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), | 74 | () -> assertThat(tester.getInferredType(c1), Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), |
74 | () -> assertThat(tester.getInferredType(c2), | 75 | () -> assertThat(tester.getInferredType(c2), |
75 | is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))), | 76 | Matchers.is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))), |
76 | () -> assertThat(tester.getInferredType(c3), is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), | 77 | () -> assertThat(tester.getInferredType(c3), Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), |
77 | () -> assertThat(tester.getInferredType(c4), is(new InferredType(Set.of(a4, c4), Set.of(c4), c4))) | 78 | () -> assertThat(tester.getInferredType(c4), Matchers.is(new InferredType(Set.of(a4, c4), Set.of(c4), c4))) |
78 | ); | 79 | ); |
79 | } | 80 | } |
80 | 81 | ||
@@ -84,8 +85,8 @@ class TypeAnalyzerExampleHierarchyTest { | |||
84 | var a3Result = tester.getPreservedType(a3); | 85 | var a3Result = tester.getPreservedType(a3); |
85 | var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2); | 86 | var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2); |
86 | assertAll( | 87 | assertAll( |
87 | () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), is(expected)), | 88 | () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)), |
88 | () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), is(expected)), | 89 | () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)), |
89 | () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())), | 90 | () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())), |
90 | () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())), | 91 | () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())), |
91 | () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE), | 92 | () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE), |
@@ -100,19 +101,19 @@ class TypeAnalyzerExampleHierarchyTest { | |||
100 | var a4Result = tester.getPreservedType(a4); | 101 | var a4Result = tester.getPreservedType(a4); |
101 | assertAll( | 102 | assertAll( |
102 | () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE), | 103 | () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE), |
103 | is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), | 104 | Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), |
104 | () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | 105 | () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE), |
105 | is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), | 106 | Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), |
106 | () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE), | 107 | () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE), |
107 | is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), | 108 | Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), |
108 | () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE), | 109 | () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE), |
109 | is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))), | 110 | Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))), |
110 | () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE), | 111 | () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE), |
111 | is(new InferredType(Set.of(), Set.of(c3, c4), null))), | 112 | Matchers.is(new InferredType(Set.of(), Set.of(c3, c4), null))), |
112 | () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE), | 113 | () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE), |
113 | is(new InferredType(Set.of(), Set.of(c1, c4), null))), | 114 | Matchers.is(new InferredType(Set.of(), Set.of(c1, c4), null))), |
114 | () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE), | 115 | () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE), |
115 | is(new InferredType(Set.of(), Set.of(c3), null))) | 116 | Matchers.is(new InferredType(Set.of(), Set.of(c3), null))) |
116 | ); | 117 | ); |
117 | } | 118 | } |
118 | 119 | ||
@@ -122,8 +123,8 @@ class TypeAnalyzerExampleHierarchyTest { | |||
122 | var a4Result = tester.getPreservedType(a4); | 123 | var a4Result = tester.getPreservedType(a4); |
123 | var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null); | 124 | var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null); |
124 | assertAll( | 125 | assertAll( |
125 | () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), is(expected)), | 126 | () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected)), |
126 | () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), is(expected)) | 127 | () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected)) |
127 | ); | 128 | ); |
128 | } | 129 | } |
129 | 130 | ||
@@ -145,9 +146,9 @@ class TypeAnalyzerExampleHierarchyTest { | |||
145 | var c3Result = tester.getPreservedType(c3); | 146 | var c3Result = tester.getPreservedType(c3); |
146 | assertAll( | 147 | assertAll( |
147 | () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE), | 148 | () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE), |
148 | is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))), | 149 | Matchers.is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))), |
149 | () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), | 150 | () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), |
150 | is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null))) | 151 | Matchers.is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null))) |
151 | ); | 152 | ); |
152 | } | 153 | } |
153 | 154 | ||
@@ -158,13 +159,13 @@ class TypeAnalyzerExampleHierarchyTest { | |||
158 | var c1Result = tester.getPreservedType(c1); | 159 | var c1Result = tester.getPreservedType(c1); |
159 | assertAll( | 160 | assertAll( |
160 | () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | 161 | () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE), |
161 | is(new InferredType(Set.of(a1, a4), Set.of(), null))), | 162 | Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null))), |
162 | () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE), | 163 | () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE), |
163 | is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), | 164 | Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), |
164 | () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE), | 165 | () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE), |
165 | is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), | 166 | Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), |
166 | () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | 167 | () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), |
167 | is(new InferredType(Set.of(a1, a4), Set.of(), null))) | 168 | Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null))) |
168 | ); | 169 | ); |
169 | } | 170 | } |
170 | 171 | ||
@@ -174,9 +175,9 @@ class TypeAnalyzerExampleHierarchyTest { | |||
174 | var a5Result = tester.getPreservedType(a5); | 175 | var a5Result = tester.getPreservedType(a5); |
175 | assertAll( | 176 | assertAll( |
176 | () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE), | 177 | () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE), |
177 | is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), | 178 | Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), |
178 | () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE), | 179 | () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE), |
179 | is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))) | 180 | Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))) |
180 | ); | 181 | ); |
181 | } | 182 | } |
182 | 183 | ||
@@ -198,9 +199,9 @@ class TypeAnalyzerExampleHierarchyTest { | |||
198 | var a5Result = tester.getPreservedType(a5); | 199 | var a5Result = tester.getPreservedType(a5); |
199 | assertAll( | 200 | assertAll( |
200 | () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR), | 201 | () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR), |
201 | is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), | 202 | Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), |
202 | () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR), | 203 | () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR), |
203 | is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), | 204 | Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), |
204 | () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR), | 205 | () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR), |
205 | is(a5Result.asInferredType())) | 206 | is(a5Result.asInferredType())) |
206 | ); | 207 | ); |
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java index d0ef9d57..315f9672 100644 --- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java | |||
@@ -5,6 +5,7 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.typehierarchy; | 6 | package tools.refinery.store.reasoning.translator.typehierarchy; |
7 | 7 | ||
8 | import org.hamcrest.Matchers; | ||
8 | import org.junit.jupiter.api.Test; | 9 | import org.junit.jupiter.api.Test; |
9 | import tools.refinery.store.reasoning.representation.PartialRelation; | 10 | import tools.refinery.store.reasoning.representation.PartialRelation; |
10 | import tools.refinery.store.representation.TruthValue; | 11 | import tools.refinery.store.representation.TruthValue; |
@@ -141,8 +142,8 @@ class TypeAnalyzerTest { | |||
141 | 142 | ||
142 | var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3); | 143 | var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3); |
143 | assertAll( | 144 | assertAll( |
144 | () -> assertThat(tester.getInferredType(c3), is(expected)), | 145 | () -> assertThat(tester.getInferredType(c3), Matchers.is(expected)), |
145 | () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(expected)) | 146 | () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), Matchers.is(expected)) |
146 | ); | 147 | ); |
147 | } | 148 | } |
148 | 149 | ||
@@ -166,7 +167,7 @@ class TypeAnalyzerTest { | |||
166 | var a1Result = tester.getPreservedType(a1); | 167 | var a1Result = tester.getPreservedType(a1); |
167 | 168 | ||
168 | assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | 169 | assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), |
169 | is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2))); | 170 | Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2))); |
170 | } | 171 | } |
171 | 172 | ||
172 | @Test | 173 | @Test |
@@ -189,7 +190,7 @@ class TypeAnalyzerTest { | |||
189 | var a1Result = tester.getPreservedType(a1); | 190 | var a1Result = tester.getPreservedType(a1); |
190 | 191 | ||
191 | assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | 192 | assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), |
192 | is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3))); | 193 | Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3))); |
193 | } | 194 | } |
194 | 195 | ||
195 | @Test | 196 | @Test |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java b/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java index 1080a248..5e69e7af 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java +++ b/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java | |||
@@ -5,6 +5,9 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.map; | 6 | package tools.refinery.store.map; |
7 | 7 | ||
8 | import java.util.Iterator; | ||
9 | import java.util.Map; | ||
10 | |||
8 | public final class Cursors { | 11 | public final class Cursors { |
9 | private Cursors() { | 12 | private Cursors() { |
10 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); | 13 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); |
@@ -18,6 +21,14 @@ public final class Cursors { | |||
18 | return new Singleton<>(key, value); | 21 | return new Singleton<>(key, value); |
19 | } | 22 | } |
20 | 23 | ||
24 | public static <K, V> Cursor<K, V> of(Iterator<Map.Entry<K, V>> iterator) { | ||
25 | return new IteratorBasedCursor<>(iterator); | ||
26 | } | ||
27 | |||
28 | public static <K, V> Cursor<K, V> of(Map<K, V> map) { | ||
29 | return of(map.entrySet().iterator()); | ||
30 | } | ||
31 | |||
21 | private static class Empty<K, V> implements Cursor<K, V> { | 32 | private static class Empty<K, V> implements Cursor<K, V> { |
22 | private boolean terminated = false; | 33 | private boolean terminated = false; |
23 | 34 | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java b/subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java new file mode 100644 index 00000000..0ed9b730 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java | |||
@@ -0,0 +1,44 @@ | |||
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.map; | ||
7 | |||
8 | import java.util.Iterator; | ||
9 | import java.util.Map; | ||
10 | |||
11 | public class IteratorBasedCursor<K, V> implements Cursor<K, V> { | ||
12 | private final Iterator<Map.Entry<K, V>> iterator; | ||
13 | private Map.Entry<K, V> entry; | ||
14 | private boolean terminated; | ||
15 | |||
16 | public IteratorBasedCursor(Iterator<Map.Entry<K, V>> iterator) { | ||
17 | this.iterator = iterator; | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public K getKey() { | ||
22 | return entry.getKey(); | ||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public V getValue() { | ||
27 | return entry.getValue(); | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public boolean isTerminated() { | ||
32 | return terminated; | ||
33 | } | ||
34 | |||
35 | @Override | ||
36 | public boolean move() { | ||
37 | if (!terminated && iterator.hasNext()) { | ||
38 | entry = iterator.next(); | ||
39 | return true; | ||
40 | } | ||
41 | terminated = true; | ||
42 | return false; | ||
43 | } | ||
44 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java index 3a4024b5..8f652762 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java +++ b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java | |||
@@ -29,7 +29,9 @@ public interface ModelStoreBuilder { | |||
29 | 29 | ||
30 | <T> ModelStoreBuilder symbol(Symbol<T> symbol); | 30 | <T> ModelStoreBuilder symbol(Symbol<T> symbol); |
31 | 31 | ||
32 | <T extends ModelAdapterBuilder> ModelStoreBuilder with(T adapterBuilder); | 32 | ModelStoreBuilder with(ModelAdapterBuilder adapterBuilder); |
33 | |||
34 | ModelStoreBuilder with(ModelStoreConfiguration configuration); | ||
33 | 35 | ||
34 | <T extends ModelAdapterBuilder> Optional<T> tryGetAdapter(Class<? extends T> adapterType); | 36 | <T extends ModelAdapterBuilder> Optional<T> tryGetAdapter(Class<? extends T> adapterType); |
35 | 37 | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java new file mode 100644 index 00000000..e94af5f8 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java | |||
@@ -0,0 +1,11 @@ | |||
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.model; | ||
7 | |||
8 | @FunctionalInterface | ||
9 | public interface ModelStoreConfiguration { | ||
10 | void apply(ModelStoreBuilder storeBuilder); | ||
11 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java b/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java index d9245c1d..3d7f59d7 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java +++ b/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java | |||
@@ -9,14 +9,9 @@ import org.eclipse.collections.api.factory.Maps; | |||
9 | import org.eclipse.collections.api.factory.primitive.IntObjectMaps; | 9 | import org.eclipse.collections.api.factory.primitive.IntObjectMaps; |
10 | import org.eclipse.collections.api.map.MutableMap; | 10 | import org.eclipse.collections.api.map.MutableMap; |
11 | import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; | 11 | import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; |
12 | import tools.refinery.store.map.AnyVersionedMap; | 12 | import tools.refinery.store.map.*; |
13 | import tools.refinery.store.map.Cursor; | ||
14 | import tools.refinery.store.map.Cursors; | ||
15 | import tools.refinery.store.map.VersionedMap; | ||
16 | import tools.refinery.store.tuple.Tuple; | 13 | import tools.refinery.store.tuple.Tuple; |
17 | 14 | ||
18 | import java.util.Iterator; | ||
19 | import java.util.Map; | ||
20 | import java.util.Set; | 15 | import java.util.Set; |
21 | 16 | ||
22 | class BaseIndexer<T> { | 17 | class BaseIndexer<T> { |
@@ -91,40 +86,12 @@ class BaseIndexer<T> { | |||
91 | return new IndexCursor<>(adjacentTuples, versionedMap); | 86 | return new IndexCursor<>(adjacentTuples, versionedMap); |
92 | } | 87 | } |
93 | 88 | ||
94 | private static class IndexCursor<T> implements Cursor<Tuple, T> { | 89 | private static class IndexCursor<T> extends IteratorBasedCursor<Tuple, T> { |
95 | private final Set<AnyVersionedMap> dependingMaps; | 90 | private final Set<AnyVersionedMap> dependingMaps; |
96 | private final Iterator<Map.Entry<Tuple, T>> iterator; | ||
97 | private Map.Entry<Tuple, T> entry; | ||
98 | private boolean terminated; | ||
99 | 91 | ||
100 | public IndexCursor(MutableMap<Tuple, T> adjacentTuples, VersionedMap<Tuple, T> versionedMap) { | 92 | public IndexCursor(MutableMap<Tuple, T> map, VersionedMap<Tuple, T> versionedMap) { |
93 | super(map.entrySet().iterator()); | ||
101 | dependingMaps = versionedMap == null ? Set.of() : Set.of(versionedMap); | 94 | dependingMaps = versionedMap == null ? Set.of() : Set.of(versionedMap); |
102 | iterator = adjacentTuples.entrySet().iterator(); | ||
103 | } | ||
104 | |||
105 | @Override | ||
106 | public Tuple getKey() { | ||
107 | return entry.getKey(); | ||
108 | } | ||
109 | |||
110 | @Override | ||
111 | public T getValue() { | ||
112 | return entry.getValue(); | ||
113 | } | ||
114 | |||
115 | @Override | ||
116 | public boolean isTerminated() { | ||
117 | return terminated; | ||
118 | } | ||
119 | |||
120 | @Override | ||
121 | public boolean move() { | ||
122 | if (!terminated && iterator.hasNext()) { | ||
123 | entry = iterator.next(); | ||
124 | return true; | ||
125 | } | ||
126 | terminated = true; | ||
127 | return false; | ||
128 | } | 95 | } |
129 | 96 | ||
130 | @Override | 97 | @Override |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java b/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java index aafbe130..5c688178 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java +++ b/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java | |||
@@ -11,6 +11,7 @@ import tools.refinery.store.map.VersionedMapStore; | |||
11 | import tools.refinery.store.map.VersionedMapStoreImpl; | 11 | import tools.refinery.store.map.VersionedMapStoreImpl; |
12 | import tools.refinery.store.model.ModelStore; | 12 | import tools.refinery.store.model.ModelStore; |
13 | import tools.refinery.store.model.ModelStoreBuilder; | 13 | import tools.refinery.store.model.ModelStoreBuilder; |
14 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
14 | import tools.refinery.store.model.TupleHashProvider; | 15 | import tools.refinery.store.model.TupleHashProvider; |
15 | import tools.refinery.store.representation.AnySymbol; | 16 | import tools.refinery.store.representation.AnySymbol; |
16 | import tools.refinery.store.representation.Symbol; | 17 | import tools.refinery.store.representation.Symbol; |
@@ -26,7 +27,8 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder { | |||
26 | @Override | 27 | @Override |
27 | public <T> ModelStoreBuilder symbol(Symbol<T> symbol) { | 28 | public <T> ModelStoreBuilder symbol(Symbol<T> symbol) { |
28 | if (!allSymbols.add(symbol)) { | 29 | if (!allSymbols.add(symbol)) { |
29 | throw new IllegalArgumentException("Symbol %s already added".formatted(symbol)); | 30 | // No need to add symbol twice. |
31 | return this; | ||
30 | } | 32 | } |
31 | var equivalenceClass = new SymbolEquivalenceClass<>(symbol); | 33 | var equivalenceClass = new SymbolEquivalenceClass<>(symbol); |
32 | var symbolsInEquivalenceClass = equivalenceClasses.computeIfAbsent(equivalenceClass, | 34 | var symbolsInEquivalenceClass = equivalenceClasses.computeIfAbsent(equivalenceClass, |
@@ -36,7 +38,7 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder { | |||
36 | } | 38 | } |
37 | 39 | ||
38 | @Override | 40 | @Override |
39 | public <T extends ModelAdapterBuilder> ModelStoreBuilder with(T adapterBuilder) { | 41 | public ModelStoreBuilder with(ModelAdapterBuilder adapterBuilder) { |
40 | for (var existingAdapter : adapters) { | 42 | for (var existingAdapter : adapters) { |
41 | if (existingAdapter.getClass().equals(adapterBuilder.getClass())) { | 43 | if (existingAdapter.getClass().equals(adapterBuilder.getClass())) { |
42 | throw new IllegalArgumentException("%s adapter was already configured for store builder" | 44 | throw new IllegalArgumentException("%s adapter was already configured for store builder" |
@@ -48,6 +50,12 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder { | |||
48 | } | 50 | } |
49 | 51 | ||
50 | @Override | 52 | @Override |
53 | public ModelStoreBuilder with(ModelStoreConfiguration configuration) { | ||
54 | configuration.apply(this); | ||
55 | return this; | ||
56 | } | ||
57 | |||
58 | @Override | ||
51 | public <T extends ModelAdapterBuilder> Optional<T> tryGetAdapter(Class<? extends T> adapterType) { | 59 | public <T extends ModelAdapterBuilder> Optional<T> tryGetAdapter(Class<? extends T> adapterType) { |
52 | return AdapterUtils.tryGetAdapter(adapters, adapterType); | 60 | return AdapterUtils.tryGetAdapter(adapters, adapterType); |
53 | } | 61 | } |
@@ -59,13 +67,14 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder { | |||
59 | 67 | ||
60 | @Override | 68 | @Override |
61 | public ModelStore build() { | 69 | public ModelStore build() { |
70 | // First configure adapters and let them register any symbols we don't know about yet. | ||
71 | for (int i = adapters.size() - 1; i >= 0; i--) { | ||
72 | adapters.get(i).configure(this); | ||
73 | } | ||
62 | var stores = new HashMap<AnySymbol, VersionedMapStore<Tuple, ?>>(allSymbols.size()); | 74 | var stores = new HashMap<AnySymbol, VersionedMapStore<Tuple, ?>>(allSymbols.size()); |
63 | for (var entry : equivalenceClasses.entrySet()) { | 75 | for (var entry : equivalenceClasses.entrySet()) { |
64 | createStores(stores, entry.getKey(), entry.getValue()); | 76 | createStores(stores, entry.getKey(), entry.getValue()); |
65 | } | 77 | } |
66 | for (int i = adapters.size() - 1; i >= 0; i--) { | ||
67 | adapters.get(i).configure(this); | ||
68 | } | ||
69 | var modelStore = new ModelStoreImpl(stores, adapters.size()); | 78 | var modelStore = new ModelStoreImpl(stores, adapters.size()); |
70 | for (var adapterBuilder : adapters) { | 79 | for (var adapterBuilder : adapters) { |
71 | var storeAdapter = adapterBuilder.build(modelStore); | 80 | var storeAdapter = adapterBuilder.build(modelStore); |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java index 52c740e8..dfdb43bd 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java | |||
@@ -5,6 +5,7 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.representation; | 6 | package tools.refinery.store.representation; |
7 | 7 | ||
8 | import java.util.Objects; | ||
8 | import java.util.Optional; | 9 | import java.util.Optional; |
9 | 10 | ||
10 | public non-sealed interface AbstractDomain<A, C> extends AnyAbstractDomain { | 11 | public non-sealed interface AbstractDomain<A, C> extends AnyAbstractDomain { |
@@ -22,7 +23,9 @@ public non-sealed interface AbstractDomain<A, C> extends AnyAbstractDomain { | |||
22 | return toConcrete(abstractValue).isPresent(); | 23 | return toConcrete(abstractValue).isPresent(); |
23 | } | 24 | } |
24 | 25 | ||
25 | boolean isRefinement(A originalValue, A refinedValue); | 26 | default boolean isRefinement(A originalValue, A refinedValue) { |
27 | return Objects.equals(commonRefinement(originalValue, refinedValue), refinedValue); | ||
28 | } | ||
26 | 29 | ||
27 | A commonRefinement(A leftValue, A rightValue); | 30 | A commonRefinement(A leftValue, A rightValue); |
28 | 31 | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java index 40baf9a5..f81ee9a4 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java | |||
@@ -36,6 +36,10 @@ public enum TruthValue { | |||
36 | return this != UNKNOWN; | 36 | return this != UNKNOWN; |
37 | } | 37 | } |
38 | 38 | ||
39 | public boolean isConcrete() { | ||
40 | return this == TRUE || this == FALSE; | ||
41 | } | ||
42 | |||
39 | public boolean must() { | 43 | public boolean must() { |
40 | return this == TRUE || this == ERROR; | 44 | return this == TRUE || this == ERROR; |
41 | } | 45 | } |
@@ -55,9 +59,18 @@ public enum TruthValue { | |||
55 | public TruthValue merge(TruthValue other) { | 59 | public TruthValue merge(TruthValue other) { |
56 | return switch (this) { | 60 | return switch (this) { |
57 | case TRUE -> other == UNKNOWN || other == TRUE ? TRUE : ERROR; | 61 | case TRUE -> other == UNKNOWN || other == TRUE ? TRUE : ERROR; |
58 | case FALSE -> other == TruthValue.UNKNOWN || other == TruthValue.FALSE ? FALSE : ERROR; | 62 | case FALSE -> other == UNKNOWN || other == FALSE ? FALSE : ERROR; |
59 | case UNKNOWN -> other; | 63 | case UNKNOWN -> other; |
60 | default -> ERROR; | 64 | case ERROR -> ERROR; |
65 | }; | ||
66 | } | ||
67 | |||
68 | public TruthValue join(TruthValue other) { | ||
69 | return switch (this) { | ||
70 | case TRUE -> other == ERROR || other == TRUE ? TRUE : UNKNOWN; | ||
71 | case FALSE -> other == ERROR || other == FALSE ? FALSE : UNKNOWN; | ||
72 | case UNKNOWN -> UNKNOWN; | ||
73 | case ERROR -> other; | ||
61 | }; | 74 | }; |
62 | } | 75 | } |
63 | } | 76 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java index 89f8dd19..61696dca 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java | |||
@@ -7,6 +7,8 @@ package tools.refinery.store.representation; | |||
7 | 7 | ||
8 | import java.util.Optional; | 8 | import java.util.Optional; |
9 | 9 | ||
10 | // Singleton pattern, because there is only one domain for truth values. | ||
11 | @SuppressWarnings("squid:S6548") | ||
10 | public final class TruthValueDomain implements AbstractDomain<TruthValue, Boolean> { | 12 | public final class TruthValueDomain implements AbstractDomain<TruthValue, Boolean> { |
11 | public static final TruthValueDomain INSTANCE = new TruthValueDomain(); | 13 | public static final TruthValueDomain INSTANCE = new TruthValueDomain(); |
12 | 14 | ||
@@ -15,51 +17,50 @@ public final class TruthValueDomain implements AbstractDomain<TruthValue, Boolea | |||
15 | 17 | ||
16 | @Override | 18 | @Override |
17 | public Class<TruthValue> abstractType() { | 19 | public Class<TruthValue> abstractType() { |
18 | return null; | 20 | return TruthValue.class; |
19 | } | 21 | } |
20 | 22 | ||
21 | @Override | 23 | @Override |
22 | public Class<Boolean> concreteType() { | 24 | public Class<Boolean> concreteType() { |
23 | return null; | 25 | return Boolean.class; |
24 | } | 26 | } |
25 | 27 | ||
26 | @Override | 28 | @Override |
27 | public TruthValue toAbstract(Boolean concreteValue) { | 29 | public TruthValue toAbstract(Boolean concreteValue) { |
28 | return null; | 30 | return TruthValue.toTruthValue(concreteValue); |
29 | } | 31 | } |
30 | 32 | ||
31 | @Override | 33 | @Override |
32 | public Optional<Boolean> toConcrete(TruthValue abstractValue) { | 34 | public Optional<Boolean> toConcrete(TruthValue abstractValue) { |
33 | return Optional.empty(); | 35 | return switch (abstractValue) { |
36 | case TRUE -> Optional.of(true); | ||
37 | case FALSE -> Optional.of(false); | ||
38 | default -> Optional.empty(); | ||
39 | }; | ||
34 | } | 40 | } |
35 | 41 | ||
36 | @Override | 42 | @Override |
37 | public boolean isConcrete(TruthValue abstractValue) { | 43 | public boolean isConcrete(TruthValue abstractValue) { |
38 | return AbstractDomain.super.isConcrete(abstractValue); | 44 | return abstractValue.isConcrete(); |
39 | } | ||
40 | |||
41 | @Override | ||
42 | public boolean isRefinement(TruthValue originalValue, TruthValue refinedValue) { | ||
43 | return false; | ||
44 | } | 45 | } |
45 | 46 | ||
46 | @Override | 47 | @Override |
47 | public TruthValue commonRefinement(TruthValue leftValue, TruthValue rightValue) { | 48 | public TruthValue commonRefinement(TruthValue leftValue, TruthValue rightValue) { |
48 | return null; | 49 | return leftValue.merge(rightValue); |
49 | } | 50 | } |
50 | 51 | ||
51 | @Override | 52 | @Override |
52 | public TruthValue commonAncestor(TruthValue leftValue, TruthValue rightValue) { | 53 | public TruthValue commonAncestor(TruthValue leftValue, TruthValue rightValue) { |
53 | return null; | 54 | return leftValue.join(rightValue); |
54 | } | 55 | } |
55 | 56 | ||
56 | @Override | 57 | @Override |
57 | public TruthValue unknown() { | 58 | public TruthValue unknown() { |
58 | return null; | 59 | return TruthValue.UNKNOWN; |
59 | } | 60 | } |
60 | 61 | ||
61 | @Override | 62 | @Override |
62 | public boolean isError(TruthValue abstractValue) { | 63 | public boolean isError(TruthValue abstractValue) { |
63 | return false; | 64 | return !abstractValue.isConsistent(); |
64 | } | 65 | } |
65 | } | 66 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java index aae7b344..e9761763 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java | |||
@@ -12,6 +12,8 @@ public sealed interface Tuple extends Comparable<Tuple> permits Tuple0, Tuple1, | |||
12 | 12 | ||
13 | int get(int element); | 13 | int get(int element); |
14 | 14 | ||
15 | Tuple set(int element, int value); | ||
16 | |||
15 | @Override | 17 | @Override |
16 | default int compareTo(@NotNull Tuple other) { | 18 | default int compareTo(@NotNull Tuple other) { |
17 | int size = getSize(); | 19 | int size = getSize(); |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java index a9aa9bf2..5f525798 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java | |||
@@ -29,6 +29,11 @@ public final class Tuple0 implements Tuple { | |||
29 | } | 29 | } |
30 | 30 | ||
31 | @Override | 31 | @Override |
32 | public Tuple set(int element, int value) { | ||
33 | throw new IndexOutOfBoundsException(element); | ||
34 | } | ||
35 | |||
36 | @Override | ||
32 | public String toString() { | 37 | public String toString() { |
33 | return TUPLE_BEGIN + TUPLE_END; | 38 | return TUPLE_BEGIN + TUPLE_END; |
34 | } | 39 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java index 388ee3a9..fb9497d2 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java | |||
@@ -38,6 +38,14 @@ public final class Tuple1 implements Tuple { | |||
38 | } | 38 | } |
39 | 39 | ||
40 | @Override | 40 | @Override |
41 | public Tuple set(int element, int value) { | ||
42 | if (element == 0) { | ||
43 | return Tuple.of(value); | ||
44 | } | ||
45 | throw new IndexOutOfBoundsException(element); | ||
46 | } | ||
47 | |||
48 | @Override | ||
41 | public String toString() { | 49 | public String toString() { |
42 | return TUPLE_BEGIN + value0 + TUPLE_END; | 50 | return TUPLE_BEGIN + value0 + TUPLE_END; |
43 | } | 51 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java index 6d886fd3..2213df97 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java | |||
@@ -25,6 +25,15 @@ public record Tuple2(int value0, int value1) implements Tuple { | |||
25 | } | 25 | } |
26 | 26 | ||
27 | @Override | 27 | @Override |
28 | public Tuple set(int element, int value) { | ||
29 | return switch (element) { | ||
30 | case 0 -> Tuple.of(value, value1); | ||
31 | case 1 -> Tuple.of(value0, value); | ||
32 | default -> throw new ArrayIndexOutOfBoundsException(element); | ||
33 | }; | ||
34 | } | ||
35 | |||
36 | @Override | ||
28 | public String toString() { | 37 | public String toString() { |
29 | return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_END; | 38 | return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_END; |
30 | } | 39 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java index 734e45c2..417770e8 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java | |||
@@ -26,6 +26,16 @@ public record Tuple3(int value0, int value1, int value2) implements Tuple { | |||
26 | } | 26 | } |
27 | 27 | ||
28 | @Override | 28 | @Override |
29 | public Tuple set(int element, int value) { | ||
30 | return switch (element) { | ||
31 | case 0 -> Tuple.of(value, value1, value2); | ||
32 | case 1 -> Tuple.of(value0, value, value2); | ||
33 | case 2 -> Tuple.of(value0, value1, value); | ||
34 | default -> throw new ArrayIndexOutOfBoundsException(element); | ||
35 | }; | ||
36 | } | ||
37 | |||
38 | @Override | ||
29 | public String toString() { | 39 | public String toString() { |
30 | return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_SEPARATOR + value2 + TUPLE_END; | 40 | return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_SEPARATOR + value2 + TUPLE_END; |
31 | } | 41 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java index e1b93e7b..c4915198 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java | |||
@@ -27,6 +27,17 @@ public record Tuple4(int value0, int value1, int value2, int value3) implements | |||
27 | } | 27 | } |
28 | 28 | ||
29 | @Override | 29 | @Override |
30 | public Tuple set(int element, int value) { | ||
31 | return switch (element) { | ||
32 | case 0 -> Tuple.of(value, value1, value2, value3); | ||
33 | case 1 -> Tuple.of(value0, value, value2, value3); | ||
34 | case 2 -> Tuple.of(value0, value1, value, value3); | ||
35 | case 3 -> Tuple.of(value0, value1, value2, value); | ||
36 | default -> throw new ArrayIndexOutOfBoundsException(element); | ||
37 | }; | ||
38 | } | ||
39 | |||
40 | @Override | ||
30 | public String toString() { | 41 | public String toString() { |
31 | return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_SEPARATOR + value2 + TUPLE_SEPARATOR + value3 + | 42 | return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_SEPARATOR + value2 + TUPLE_SEPARATOR + value3 + |
32 | TUPLE_END; | 43 | TUPLE_END; |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java index b66af491..b42b4b6a 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java | |||
@@ -32,6 +32,16 @@ public final class TupleN implements Tuple { | |||
32 | } | 32 | } |
33 | 33 | ||
34 | @Override | 34 | @Override |
35 | public Tuple set(int element, int value) { | ||
36 | int size = getSize(); | ||
37 | var newValues = new int[size]; | ||
38 | for (int i = 0; i < size; i++) { | ||
39 | newValues[i] = element == i ? value : values[i]; | ||
40 | } | ||
41 | return Tuple.of(newValues); | ||
42 | } | ||
43 | |||
44 | @Override | ||
35 | public String toString() { | 45 | public String toString() { |
36 | var valuesString = Arrays.stream(values) | 46 | var valuesString = Arrays.stream(values) |
37 | .mapToObj(Integer::toString) | 47 | .mapToObj(Integer::toString) |