diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-02-25 00:55:36 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-02-25 00:56:29 +0100 |
commit | 71372b4d57b1c51cd892aa07343c3dbc8de3e727 (patch) | |
tree | ae3fadaa0a2558dd4c7c0779e399435c7f30f5ba /subprojects/store-reasoning | |
parent | feat: Dnf reduction and structural equality (diff) | |
download | refinery-71372b4d57b1c51cd892aa07343c3dbc8de3e727.tar.gz refinery-71372b4d57b1c51cd892aa07343c3dbc8de3e727.tar.zst refinery-71372b4d57b1c51cd892aa07343c3dbc8de3e727.zip |
refactor: rename PartialInterpretation adapter
Diffstat (limited to 'subprojects/store-reasoning')
47 files changed, 2213 insertions, 0 deletions
diff --git a/subprojects/store-reasoning/build.gradle b/subprojects/store-reasoning/build.gradle new file mode 100644 index 00000000..cb440d9f --- /dev/null +++ b/subprojects/store-reasoning/build.gradle | |||
@@ -0,0 +1,7 @@ | |||
1 | plugins { | ||
2 | id 'refinery-java-library' | ||
3 | } | ||
4 | |||
5 | dependencies { | ||
6 | api project(':refinery-store-query') | ||
7 | } | ||
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/AnyPartialInterpretation.java new file mode 100644 index 00000000..ebe82c8b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java | |||
@@ -0,0 +1,13 @@ | |||
1 | package tools.refinery.store.reasoning; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
4 | |||
5 | public sealed interface AnyPartialInterpretation permits PartialInterpretation { | ||
6 | ReasoningAdapter getAdapter(); | ||
7 | |||
8 | AnyPartialSymbol getPartialSymbol(); | ||
9 | |||
10 | int countUnfinished(); | ||
11 | |||
12 | int countErrors(); | ||
13 | } | ||
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 new file mode 100644 index 00000000..0d51598b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java | |||
@@ -0,0 +1,15 @@ | |||
1 | package tools.refinery.store.reasoning; | ||
2 | |||
3 | public enum MergeResult { | ||
4 | UNCHANGED, | ||
5 | REFINED, | ||
6 | REJECTED; | ||
7 | |||
8 | public MergeResult andAlso(MergeResult other) { | ||
9 | return switch (this) { | ||
10 | case UNCHANGED -> other; | ||
11 | case REFINED -> other == REJECTED ? REJECTED : REFINED; | ||
12 | case REJECTED -> REJECTED; | ||
13 | }; | ||
14 | } | ||
15 | } | ||
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/PartialInterpretation.java new file mode 100644 index 00000000..99656da8 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java | |||
@@ -0,0 +1,22 @@ | |||
1 | package tools.refinery.store.reasoning; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
4 | import tools.refinery.store.map.Cursor; | ||
5 | import tools.refinery.store.tuple.Tuple; | ||
6 | |||
7 | public non-sealed interface PartialInterpretation<A, C> extends AnyPartialInterpretation { | ||
8 | @Override | ||
9 | PartialSymbol<A, C> getPartialSymbol(); | ||
10 | |||
11 | A get(Tuple key); | ||
12 | |||
13 | Cursor<Tuple, A> getAll(); | ||
14 | |||
15 | Cursor<Tuple, A> getAllErrors(); | ||
16 | |||
17 | MergeResult merge(Tuple key, A value); | ||
18 | |||
19 | C getConcrete(Tuple key); | ||
20 | |||
21 | Cursor<Tuple, C> getAllConcrete(); | ||
22 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/Reasoning.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/Reasoning.java new file mode 100644 index 00000000..d7d0a999 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/Reasoning.java | |||
@@ -0,0 +1,24 @@ | |||
1 | package tools.refinery.store.reasoning; | ||
2 | |||
3 | import tools.refinery.store.reasoning.internal.ReasoningBuilderImpl; | ||
4 | import tools.refinery.store.adapter.ModelAdapterBuilderFactory; | ||
5 | import tools.refinery.store.model.ModelStoreBuilder; | ||
6 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
7 | |||
8 | public final class Reasoning extends ModelAdapterBuilderFactory<ReasoningAdapter, | ||
9 | ReasoningStoreAdapter, ReasoningBuilder> { | ||
10 | public static final Reasoning ADAPTER = new Reasoning(); | ||
11 | |||
12 | public static final PartialRelation EXISTS = new PartialRelation("exists", 1); | ||
13 | |||
14 | public static final PartialRelation EQUALS = new PartialRelation("equals", 1); | ||
15 | |||
16 | private Reasoning() { | ||
17 | super(ReasoningAdapter.class, ReasoningStoreAdapter.class, ReasoningBuilder.class); | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public ReasoningBuilder createBuilder(ModelStoreBuilder storeBuilder) { | ||
22 | return new ReasoningBuilderImpl(storeBuilder); | ||
23 | } | ||
24 | } | ||
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 new file mode 100644 index 00000000..e602242e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java | |||
@@ -0,0 +1,22 @@ | |||
1 | package tools.refinery.store.reasoning; | ||
2 | |||
3 | import tools.refinery.store.adapter.ModelAdapter; | ||
4 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
5 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
6 | import tools.refinery.store.query.Dnf; | ||
7 | import tools.refinery.store.query.ResultSet; | ||
8 | |||
9 | public interface ReasoningAdapter extends ModelAdapter { | ||
10 | @Override | ||
11 | ReasoningStoreAdapter getStoreAdapter(); | ||
12 | |||
13 | default AnyPartialInterpretation getPartialInterpretation(AnyPartialSymbol partialSymbol) { | ||
14 | // Cast to disambiguate overloads. | ||
15 | var typedPartialSymbol = (PartialSymbol<?, ?>) partialSymbol; | ||
16 | return getPartialInterpretation(typedPartialSymbol); | ||
17 | } | ||
18 | |||
19 | <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol); | ||
20 | |||
21 | ResultSet getLiftedResultSet(Dnf query); | ||
22 | } | ||
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 new file mode 100644 index 00000000..588c2711 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java | |||
@@ -0,0 +1,28 @@ | |||
1 | package tools.refinery.store.reasoning; | ||
2 | |||
3 | import tools.refinery.store.adapter.ModelAdapterBuilder; | ||
4 | import tools.refinery.store.model.ModelStore; | ||
5 | import tools.refinery.store.reasoning.literal.Modality; | ||
6 | import tools.refinery.store.query.Dnf; | ||
7 | |||
8 | import java.util.Collection; | ||
9 | import java.util.List; | ||
10 | |||
11 | @SuppressWarnings("UnusedReturnValue") | ||
12 | public interface ReasoningBuilder extends ModelAdapterBuilder { | ||
13 | default ReasoningBuilder liftedQueries(Dnf... liftedQueries) { | ||
14 | return liftedQueries(List.of(liftedQueries)); | ||
15 | } | ||
16 | |||
17 | default ReasoningBuilder liftedQueries(Collection<Dnf> liftedQueries) { | ||
18 | liftedQueries.forEach(this::liftedQuery); | ||
19 | return this; | ||
20 | } | ||
21 | |||
22 | ReasoningBuilder liftedQuery(Dnf liftedQuery); | ||
23 | |||
24 | Dnf lift(Modality modality, Dnf query); | ||
25 | |||
26 | @Override | ||
27 | ReasoningStoreAdapter createStoreAdapter(ModelStore store); | ||
28 | } | ||
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 new file mode 100644 index 00000000..69c0f5eb --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java | |||
@@ -0,0 +1,17 @@ | |||
1 | package tools.refinery.store.reasoning; | ||
2 | |||
3 | import tools.refinery.store.adapter.ModelStoreAdapter; | ||
4 | import tools.refinery.store.model.Model; | ||
5 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
6 | import tools.refinery.store.query.Dnf; | ||
7 | |||
8 | import java.util.Collection; | ||
9 | |||
10 | public interface ReasoningStoreAdapter extends ModelStoreAdapter { | ||
11 | Collection<AnyPartialSymbol> getPartialSymbols(); | ||
12 | |||
13 | Collection<Dnf> getLiftedQueries(); | ||
14 | |||
15 | @Override | ||
16 | ReasoningAdapter createModelAdapter(Model model); | ||
17 | } | ||
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 new file mode 100644 index 00000000..a7a56680 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java | |||
@@ -0,0 +1,38 @@ | |||
1 | package tools.refinery.store.reasoning.internal; | ||
2 | |||
3 | import tools.refinery.store.model.Model; | ||
4 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
5 | import tools.refinery.store.reasoning.PartialInterpretation; | ||
6 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
7 | import tools.refinery.store.query.Dnf; | ||
8 | import tools.refinery.store.query.ResultSet; | ||
9 | |||
10 | public class ReasoningAdapterImpl implements ReasoningAdapter { | ||
11 | private final Model model; | ||
12 | private final ReasoningStoreAdapterImpl storeAdapter; | ||
13 | |||
14 | ReasoningAdapterImpl(Model model, ReasoningStoreAdapterImpl storeAdapter) { | ||
15 | this.model = model; | ||
16 | this.storeAdapter = storeAdapter; | ||
17 | } | ||
18 | |||
19 | @Override | ||
20 | public Model getModel() { | ||
21 | return model; | ||
22 | } | ||
23 | |||
24 | @Override | ||
25 | public ReasoningStoreAdapterImpl getStoreAdapter() { | ||
26 | return storeAdapter; | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) { | ||
31 | return null; | ||
32 | } | ||
33 | |||
34 | @Override | ||
35 | public ResultSet getLiftedResultSet(Dnf query) { | ||
36 | return null; | ||
37 | } | ||
38 | } | ||
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 new file mode 100644 index 00000000..2860e2b9 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java | |||
@@ -0,0 +1,29 @@ | |||
1 | package tools.refinery.store.reasoning.internal; | ||
2 | |||
3 | import tools.refinery.store.adapter.AbstractModelAdapterBuilder; | ||
4 | import tools.refinery.store.model.ModelStore; | ||
5 | import tools.refinery.store.model.ModelStoreBuilder; | ||
6 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
7 | import tools.refinery.store.reasoning.literal.Modality; | ||
8 | import tools.refinery.store.query.Dnf; | ||
9 | |||
10 | public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder implements ReasoningBuilder { | ||
11 | public ReasoningBuilderImpl(ModelStoreBuilder storeBuilder) { | ||
12 | super(storeBuilder); | ||
13 | } | ||
14 | |||
15 | @Override | ||
16 | public ReasoningBuilder liftedQuery(Dnf liftedQuery) { | ||
17 | return null; | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public Dnf lift(Modality modality, Dnf query) { | ||
22 | return null; | ||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public ReasoningStoreAdapterImpl createStoreAdapter(ModelStore store) { | ||
27 | return null; | ||
28 | } | ||
29 | } | ||
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 new file mode 100644 index 00000000..763dad6d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java | |||
@@ -0,0 +1,37 @@ | |||
1 | package tools.refinery.store.reasoning.internal; | ||
2 | |||
3 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
4 | import tools.refinery.store.model.Model; | ||
5 | import tools.refinery.store.model.ModelStore; | ||
6 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
7 | import tools.refinery.store.query.Dnf; | ||
8 | |||
9 | import java.util.Collection; | ||
10 | |||
11 | public class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { | ||
12 | private final ModelStore store; | ||
13 | |||
14 | ReasoningStoreAdapterImpl(ModelStore store) { | ||
15 | this.store = store; | ||
16 | } | ||
17 | |||
18 | @Override | ||
19 | public ModelStore getStore() { | ||
20 | return store; | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public Collection<AnyPartialSymbol> getPartialSymbols() { | ||
25 | return null; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public Collection<Dnf> getLiftedQueries() { | ||
30 | return null; | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public ReasoningAdapterImpl createModelAdapter(Model model) { | ||
35 | return new ReasoningAdapterImpl(model, this); | ||
36 | } | ||
37 | } | ||
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 new file mode 100644 index 00000000..966e080a --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java | |||
@@ -0,0 +1,107 @@ | |||
1 | package tools.refinery.store.reasoning.lifting; | ||
2 | |||
3 | import org.jetbrains.annotations.Nullable; | ||
4 | import tools.refinery.store.reasoning.literal.ModalDnfCallLiteral; | ||
5 | import tools.refinery.store.reasoning.Reasoning; | ||
6 | import tools.refinery.store.reasoning.literal.ModalRelationLiteral; | ||
7 | import tools.refinery.store.reasoning.literal.PartialRelationLiteral; | ||
8 | import tools.refinery.store.query.Dnf; | ||
9 | import tools.refinery.store.query.DnfBuilder; | ||
10 | import tools.refinery.store.query.DnfClause; | ||
11 | import tools.refinery.store.query.Variable; | ||
12 | import tools.refinery.store.query.literal.CallPolarity; | ||
13 | import tools.refinery.store.query.literal.DnfCallLiteral; | ||
14 | import tools.refinery.store.query.literal.Literal; | ||
15 | import tools.refinery.store.reasoning.literal.Modality; | ||
16 | import tools.refinery.store.util.CycleDetectingMapper; | ||
17 | |||
18 | import java.util.ArrayList; | ||
19 | import java.util.HashSet; | ||
20 | import java.util.List; | ||
21 | |||
22 | public class DnfLifter { | ||
23 | private final CycleDetectingMapper<ModalDnf, Dnf> mapper = new CycleDetectingMapper<>(ModalDnf::toString, | ||
24 | this::doLift); | ||
25 | |||
26 | public Dnf lift(Modality modality, Dnf query) { | ||
27 | return mapper.map(new ModalDnf(modality, query)); | ||
28 | } | ||
29 | |||
30 | private Dnf doLift(ModalDnf modalDnf) { | ||
31 | var modality = modalDnf.modality(); | ||
32 | var dnf = modalDnf.dnf(); | ||
33 | var builder = Dnf.builder(); | ||
34 | builder.parameters(dnf.getParameters()); | ||
35 | boolean changed = false; | ||
36 | for (var clause : dnf.getClauses()) { | ||
37 | if (liftClause(modality, clause, builder)) { | ||
38 | changed = true; | ||
39 | } | ||
40 | } | ||
41 | if (changed) { | ||
42 | return builder.build(); | ||
43 | } | ||
44 | return dnf; | ||
45 | } | ||
46 | |||
47 | private boolean liftClause(Modality modality, DnfClause clause, DnfBuilder builder) { | ||
48 | boolean changed = false; | ||
49 | var quantifiedVariables = new HashSet<>(clause.quantifiedVariables()); | ||
50 | var literals = clause.literals(); | ||
51 | var liftedLiterals = new ArrayList<Literal>(literals.size()); | ||
52 | for (var literal : literals) { | ||
53 | Literal liftedLiteral = liftLiteral(modality, literal); | ||
54 | if (liftedLiteral == null) { | ||
55 | liftedLiteral = literal; | ||
56 | } else { | ||
57 | changed = true; | ||
58 | } | ||
59 | liftedLiterals.add(liftedLiteral); | ||
60 | var variable = isExistsLiteralForVariable(modality, liftedLiteral); | ||
61 | if (variable != null) { | ||
62 | // If we already quantify over the existence of the variable with the expected modality, | ||
63 | // we don't need to insert quantification manually. | ||
64 | quantifiedVariables.remove(variable); | ||
65 | } | ||
66 | } | ||
67 | for (var quantifiedVariable : quantifiedVariables) { | ||
68 | // Quantify over variables that are not already quantified with the expected modality. | ||
69 | liftedLiterals.add(Reasoning.EXISTS.call(CallPolarity.POSITIVE, modality, | ||
70 | List.of(quantifiedVariable))); | ||
71 | } | ||
72 | builder.clause(liftedLiterals); | ||
73 | return changed || !quantifiedVariables.isEmpty(); | ||
74 | } | ||
75 | |||
76 | @Nullable | ||
77 | private Variable isExistsLiteralForVariable(Modality modality, Literal literal) { | ||
78 | if (literal instanceof ModalRelationLiteral modalRelationLiteral && | ||
79 | modalRelationLiteral.getPolarity() == CallPolarity.POSITIVE && | ||
80 | modalRelationLiteral.getModality() == modality && | ||
81 | modalRelationLiteral.getTarget().equals(Reasoning.EXISTS)) { | ||
82 | return modalRelationLiteral.getArguments().get(0); | ||
83 | } | ||
84 | return null; | ||
85 | } | ||
86 | |||
87 | @Nullable | ||
88 | private Literal liftLiteral(Modality modality, Literal literal) { | ||
89 | if (literal instanceof PartialRelationLiteral partialRelationLiteral) { | ||
90 | return new ModalRelationLiteral(modality, partialRelationLiteral); | ||
91 | } else if (literal instanceof DnfCallLiteral dnfCallLiteral) { | ||
92 | var polarity = dnfCallLiteral.getPolarity(); | ||
93 | var target = dnfCallLiteral.getTarget(); | ||
94 | var liftedTarget = lift(modality.commute(polarity), target); | ||
95 | if (target.equals(liftedTarget)) { | ||
96 | return null; | ||
97 | } | ||
98 | return new DnfCallLiteral(polarity, liftedTarget, dnfCallLiteral.getArguments()); | ||
99 | } else if (literal instanceof ModalDnfCallLiteral modalDnfCallLiteral) { | ||
100 | var liftedTarget = lift(modalDnfCallLiteral.getModality(), modalDnfCallLiteral.getTarget()); | ||
101 | return new DnfCallLiteral(modalDnfCallLiteral.getPolarity(), liftedTarget, | ||
102 | modalDnfCallLiteral.getArguments()); | ||
103 | } else { | ||
104 | return null; | ||
105 | } | ||
106 | } | ||
107 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java new file mode 100644 index 00000000..7aa98bf2 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java | |||
@@ -0,0 +1,11 @@ | |||
1 | package tools.refinery.store.reasoning.lifting; | ||
2 | |||
3 | import tools.refinery.store.query.Dnf; | ||
4 | import tools.refinery.store.reasoning.literal.Modality; | ||
5 | |||
6 | public record ModalDnf(Modality modality, Dnf dnf) { | ||
7 | @Override | ||
8 | public String toString() { | ||
9 | return "%s %s".formatted(modality, dnf.name()); | ||
10 | } | ||
11 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java new file mode 100644 index 00000000..1090f1ae --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java | |||
@@ -0,0 +1,48 @@ | |||
1 | package tools.refinery.store.reasoning.literal; | ||
2 | |||
3 | import tools.refinery.store.query.Dnf; | ||
4 | import tools.refinery.store.query.Variable; | ||
5 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
6 | import tools.refinery.store.query.literal.CallPolarity; | ||
7 | import tools.refinery.store.query.literal.DnfCallLiteral; | ||
8 | import tools.refinery.store.query.literal.LiteralReduction; | ||
9 | import tools.refinery.store.query.literal.PolarLiteral; | ||
10 | import tools.refinery.store.query.substitution.Substitution; | ||
11 | |||
12 | import java.util.List; | ||
13 | |||
14 | public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiteral<ModalDnfCallLiteral> { | ||
15 | public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List<Variable> arguments) { | ||
16 | super(polarity, modality, target, arguments); | ||
17 | } | ||
18 | |||
19 | public ModalDnfCallLiteral(Modality modality, DnfCallLiteral baseLiteral) { | ||
20 | super(modality.commute(baseLiteral.getPolarity()), baseLiteral); | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public Class<Dnf> getTargetType() { | ||
25 | return Dnf.class; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) { | ||
30 | return helper.dnfEqual(getTarget(), otherTarget); | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public ModalDnfCallLiteral substitute(Substitution substitution) { | ||
35 | return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); | ||
36 | } | ||
37 | |||
38 | @Override | ||
39 | public ModalDnfCallLiteral negate() { | ||
40 | return new ModalDnfCallLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); | ||
41 | } | ||
42 | |||
43 | @Override | ||
44 | public LiteralReduction getReduction() { | ||
45 | var dnfReduction = getTarget().getReduction(); | ||
46 | return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate(); | ||
47 | } | ||
48 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java new file mode 100644 index 00000000..5992f172 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java | |||
@@ -0,0 +1,63 @@ | |||
1 | package tools.refinery.store.reasoning.literal; | ||
2 | |||
3 | import tools.refinery.store.query.RelationLike; | ||
4 | import tools.refinery.store.query.Variable; | ||
5 | import tools.refinery.store.query.equality.LiteralEqualityHelper; | ||
6 | import tools.refinery.store.query.literal.CallLiteral; | ||
7 | import tools.refinery.store.query.literal.CallPolarity; | ||
8 | import tools.refinery.store.query.literal.Literal; | ||
9 | |||
10 | import java.util.List; | ||
11 | import java.util.Objects; | ||
12 | |||
13 | public abstract class ModalLiteral<T extends RelationLike> extends CallLiteral<T> { | ||
14 | private final Modality modality; | ||
15 | |||
16 | protected ModalLiteral(CallPolarity polarity, Modality modality, T target, List<Variable> arguments) { | ||
17 | super(polarity, target, arguments); | ||
18 | this.modality = modality; | ||
19 | } | ||
20 | |||
21 | protected ModalLiteral(Modality modality, CallLiteral<? extends T> baseLiteral) { | ||
22 | this(baseLiteral.getPolarity(), commute(modality, baseLiteral.getPolarity()), baseLiteral.getTarget(), | ||
23 | baseLiteral.getArguments()); | ||
24 | } | ||
25 | |||
26 | public Modality getModality() { | ||
27 | return modality; | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) { | ||
32 | if (!super.equalsWithSubstitution(helper, other)) { | ||
33 | return false; | ||
34 | } | ||
35 | // If {@link CallLiteral#equalsWithSubstitution(LiteralEqualityHelper, Literal)} has returned {@code true}, | ||
36 | // we must have the same dynamic type as {@code other}. | ||
37 | var otherModalLiteral = (ModalLiteral<?>) other; | ||
38 | return modality == otherModalLiteral.modality; | ||
39 | } | ||
40 | |||
41 | @Override | ||
42 | protected String targetToString() { | ||
43 | return "%s %s".formatted(modality, super.targetToString()); | ||
44 | } | ||
45 | |||
46 | @Override | ||
47 | public boolean equals(Object o) { | ||
48 | if (this == o) return true; | ||
49 | if (o == null || getClass() != o.getClass()) return false; | ||
50 | if (!super.equals(o)) return false; | ||
51 | ModalLiteral<?> that = (ModalLiteral<?>) o; | ||
52 | return modality == that.modality; | ||
53 | } | ||
54 | |||
55 | @Override | ||
56 | public int hashCode() { | ||
57 | return Objects.hash(super.hashCode(), modality); | ||
58 | } | ||
59 | |||
60 | private static Modality commute(Modality modality, CallPolarity polarity) { | ||
61 | return polarity.isPositive() ? modality : modality.negate(); | ||
62 | } | ||
63 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java new file mode 100644 index 00000000..9c72bd37 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java | |||
@@ -0,0 +1,37 @@ | |||
1 | package tools.refinery.store.reasoning.literal; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
4 | import tools.refinery.store.query.Variable; | ||
5 | import tools.refinery.store.query.literal.CallPolarity; | ||
6 | import tools.refinery.store.query.literal.PolarLiteral; | ||
7 | import tools.refinery.store.query.substitution.Substitution; | ||
8 | |||
9 | import java.util.List; | ||
10 | |||
11 | public final class ModalRelationLiteral extends ModalLiteral<PartialRelation> | ||
12 | implements PolarLiteral<ModalRelationLiteral> { | ||
13 | public ModalRelationLiteral(CallPolarity polarity, Modality modality, PartialRelation target, | ||
14 | List<Variable> arguments) { | ||
15 | super(polarity, modality, target, arguments); | ||
16 | } | ||
17 | |||
18 | |||
19 | public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) { | ||
20 | super(modality, baseLiteral); | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public Class<PartialRelation> getTargetType() { | ||
25 | return PartialRelation.class; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public ModalRelationLiteral substitute(Substitution substitution) { | ||
30 | return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public ModalRelationLiteral negate() { | ||
35 | return new ModalRelationLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); | ||
36 | } | ||
37 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java new file mode 100644 index 00000000..f0cb59de --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java | |||
@@ -0,0 +1,31 @@ | |||
1 | package tools.refinery.store.reasoning.literal; | ||
2 | |||
3 | import tools.refinery.store.query.literal.CallPolarity; | ||
4 | |||
5 | import java.util.Locale; | ||
6 | |||
7 | public enum Modality { | ||
8 | MUST, | ||
9 | MAY, | ||
10 | CURRENT; | ||
11 | |||
12 | public Modality negate() { | ||
13 | return switch(this) { | ||
14 | case MUST -> MAY; | ||
15 | case MAY -> MUST; | ||
16 | case CURRENT -> CURRENT; | ||
17 | }; | ||
18 | } | ||
19 | |||
20 | public Modality commute(CallPolarity polarity) { | ||
21 | if (polarity.isPositive()) { | ||
22 | return this; | ||
23 | } | ||
24 | return this.negate(); | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public String toString() { | ||
29 | return name().toLowerCase(Locale.ROOT); | ||
30 | } | ||
31 | } | ||
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 new file mode 100644 index 00000000..10e4c7f7 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java | |||
@@ -0,0 +1,33 @@ | |||
1 | package tools.refinery.store.reasoning.literal; | ||
2 | |||
3 | import tools.refinery.store.query.literal.DnfCallLiteral; | ||
4 | |||
5 | public final class PartialLiterals { | ||
6 | private PartialLiterals() { | ||
7 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); | ||
8 | } | ||
9 | |||
10 | public ModalRelationLiteral may(PartialRelationLiteral literal) { | ||
11 | return new ModalRelationLiteral(Modality.MAY, literal); | ||
12 | } | ||
13 | |||
14 | public ModalRelationLiteral must(PartialRelationLiteral literal) { | ||
15 | return new ModalRelationLiteral(Modality.MUST, literal); | ||
16 | } | ||
17 | |||
18 | public ModalRelationLiteral current(PartialRelationLiteral literal) { | ||
19 | return new ModalRelationLiteral(Modality.CURRENT, literal); | ||
20 | } | ||
21 | |||
22 | public ModalDnfCallLiteral may(DnfCallLiteral literal) { | ||
23 | return new ModalDnfCallLiteral(Modality.MAY, literal); | ||
24 | } | ||
25 | |||
26 | public ModalDnfCallLiteral must(DnfCallLiteral literal) { | ||
27 | return new ModalDnfCallLiteral(Modality.MUST, literal); | ||
28 | } | ||
29 | |||
30 | public ModalDnfCallLiteral current(DnfCallLiteral literal) { | ||
31 | return new ModalDnfCallLiteral(Modality.CURRENT, literal); | ||
32 | } | ||
33 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java new file mode 100644 index 00000000..aff84538 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java | |||
@@ -0,0 +1,32 @@ | |||
1 | package tools.refinery.store.reasoning.literal; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
4 | import tools.refinery.store.query.Variable; | ||
5 | import tools.refinery.store.query.literal.CallLiteral; | ||
6 | import tools.refinery.store.query.literal.CallPolarity; | ||
7 | import tools.refinery.store.query.literal.PolarLiteral; | ||
8 | import tools.refinery.store.query.substitution.Substitution; | ||
9 | |||
10 | import java.util.List; | ||
11 | |||
12 | public final class PartialRelationLiteral extends CallLiteral<PartialRelation> | ||
13 | implements PolarLiteral<PartialRelationLiteral> { | ||
14 | public PartialRelationLiteral(CallPolarity polarity, PartialRelation target, List<Variable> substitution) { | ||
15 | super(polarity, target, substitution); | ||
16 | } | ||
17 | |||
18 | @Override | ||
19 | public Class<PartialRelation> getTargetType() { | ||
20 | return PartialRelation.class; | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public PartialRelationLiteral substitute(Substitution substitution) { | ||
25 | return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public PartialRelationLiteral negate() { | ||
30 | return new PartialRelationLiteral(getPolarity().negate(), getTarget(), getArguments()); | ||
31 | } | ||
32 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialFunction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialFunction.java new file mode 100644 index 00000000..e74cd58b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialFunction.java | |||
@@ -0,0 +1,4 @@ | |||
1 | package tools.refinery.store.reasoning.representation; | ||
2 | |||
3 | public sealed interface AnyPartialFunction extends AnyPartialSymbol permits PartialFunction { | ||
4 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialSymbol.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialSymbol.java new file mode 100644 index 00000000..6ff5031b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialSymbol.java | |||
@@ -0,0 +1,11 @@ | |||
1 | package tools.refinery.store.reasoning.representation; | ||
2 | |||
3 | import tools.refinery.store.representation.AnyAbstractDomain; | ||
4 | |||
5 | public sealed interface AnyPartialSymbol permits AnyPartialFunction, PartialSymbol { | ||
6 | String name(); | ||
7 | |||
8 | int arity(); | ||
9 | |||
10 | AnyAbstractDomain abstractDomain(); | ||
11 | } | ||
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 new file mode 100644 index 00000000..59eeeefe --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java | |||
@@ -0,0 +1,32 @@ | |||
1 | package tools.refinery.store.reasoning.representation; | ||
2 | |||
3 | import tools.refinery.store.representation.AbstractDomain; | ||
4 | |||
5 | public record PartialFunction<A, C>(String name, int arity, AbstractDomain<A, C> abstractDomain) | ||
6 | implements AnyPartialFunction, PartialSymbol<A, C> { | ||
7 | @Override | ||
8 | public A defaultValue() { | ||
9 | return null; | ||
10 | } | ||
11 | |||
12 | @Override | ||
13 | public C defaultConcreteValue() { | ||
14 | return null; | ||
15 | } | ||
16 | |||
17 | @Override | ||
18 | public boolean equals(Object o) { | ||
19 | return this == o; | ||
20 | } | ||
21 | |||
22 | @Override | ||
23 | public int hashCode() { | ||
24 | // Compare by identity to make hash table lookups more efficient. | ||
25 | return System.identityHashCode(this); | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public String toString() { | ||
30 | return "%s/%d".formatted(name, arity); | ||
31 | } | ||
32 | } | ||
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 new file mode 100644 index 00000000..f884f8d6 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java | |||
@@ -0,0 +1,66 @@ | |||
1 | package tools.refinery.store.reasoning.representation; | ||
2 | |||
3 | import tools.refinery.store.reasoning.literal.Modality; | ||
4 | import tools.refinery.store.reasoning.literal.PartialRelationLiteral; | ||
5 | import tools.refinery.store.reasoning.literal.ModalRelationLiteral; | ||
6 | import tools.refinery.store.query.RelationLike; | ||
7 | import tools.refinery.store.query.Variable; | ||
8 | import tools.refinery.store.query.literal.CallPolarity; | ||
9 | import tools.refinery.store.representation.AbstractDomain; | ||
10 | import tools.refinery.store.representation.TruthValue; | ||
11 | import tools.refinery.store.representation.TruthValueDomain; | ||
12 | |||
13 | import java.util.List; | ||
14 | |||
15 | public record PartialRelation(String name, int arity) implements PartialSymbol<TruthValue, Boolean>, RelationLike { | ||
16 | @Override | ||
17 | public AbstractDomain<TruthValue, Boolean> abstractDomain() { | ||
18 | return TruthValueDomain.INSTANCE; | ||
19 | } | ||
20 | |||
21 | @Override | ||
22 | public TruthValue defaultValue() { | ||
23 | return TruthValue.FALSE; | ||
24 | } | ||
25 | |||
26 | @Override | ||
27 | public Boolean defaultConcreteValue() { | ||
28 | return false; | ||
29 | } | ||
30 | |||
31 | public ModalRelationLiteral call(CallPolarity polarity, Modality modality, List<Variable> arguments) { | ||
32 | return new ModalRelationLiteral(polarity, modality, this, arguments); | ||
33 | } | ||
34 | |||
35 | public PartialRelationLiteral call(CallPolarity polarity, List<Variable> arguments) { | ||
36 | return new PartialRelationLiteral(polarity, this, arguments); | ||
37 | } | ||
38 | |||
39 | public PartialRelationLiteral call(CallPolarity polarity, Variable... arguments) { | ||
40 | return call(polarity, List.of(arguments)); | ||
41 | } | ||
42 | |||
43 | public PartialRelationLiteral call(Variable... arguments) { | ||
44 | return call(CallPolarity.POSITIVE, arguments); | ||
45 | } | ||
46 | |||
47 | public PartialRelationLiteral callTransitive(Variable left, Variable right) { | ||
48 | return call(CallPolarity.TRANSITIVE, List.of(left, right)); | ||
49 | } | ||
50 | |||
51 | @Override | ||
52 | public boolean equals(Object o) { | ||
53 | return this == o; | ||
54 | } | ||
55 | |||
56 | @Override | ||
57 | public int hashCode() { | ||
58 | // Compare by identity to make hash table lookups more efficient. | ||
59 | return System.identityHashCode(this); | ||
60 | } | ||
61 | |||
62 | @Override | ||
63 | public String toString() { | ||
64 | return "%s/%d".formatted(name, arity); | ||
65 | } | ||
66 | } | ||
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 new file mode 100644 index 00000000..1af11f2e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java | |||
@@ -0,0 +1,12 @@ | |||
1 | package tools.refinery.store.reasoning.representation; | ||
2 | |||
3 | import tools.refinery.store.representation.AbstractDomain; | ||
4 | |||
5 | public sealed interface PartialSymbol<A, C> extends AnyPartialSymbol permits PartialFunction, PartialRelation { | ||
6 | @Override | ||
7 | AbstractDomain<A, C> abstractDomain(); | ||
8 | |||
9 | A defaultValue(); | ||
10 | |||
11 | C defaultConcreteValue(); | ||
12 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java new file mode 100644 index 00000000..c7681b53 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java | |||
@@ -0,0 +1,36 @@ | |||
1 | package tools.refinery.store.reasoning.rule; | ||
2 | |||
3 | import tools.refinery.store.reasoning.Reasoning; | ||
4 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
5 | import tools.refinery.store.model.Model; | ||
6 | import tools.refinery.store.query.Variable; | ||
7 | import tools.refinery.store.representation.TruthValue; | ||
8 | import tools.refinery.store.tuple.Tuple; | ||
9 | |||
10 | import java.util.List; | ||
11 | |||
12 | public record RelationRefinementAction(PartialRelation target, List<Variable> arguments, TruthValue value) | ||
13 | implements RuleAction { | ||
14 | public RelationRefinementAction { | ||
15 | if (arguments.size() != target.arity()) { | ||
16 | throw new IllegalArgumentException("%s needs %d parameters, but got %s".formatted(target.name(), | ||
17 | target.arity(), arguments.size())); | ||
18 | } | ||
19 | if (value == TruthValue.UNKNOWN) { | ||
20 | throw new IllegalArgumentException("Refining with UNKNOWN has no effect"); | ||
21 | } | ||
22 | } | ||
23 | |||
24 | @Override | ||
25 | public RuleActionExecutor createExecutor(int[] argumentIndices, Model model) { | ||
26 | var targetInterpretation = model.getAdapter(Reasoning.ADAPTER).getPartialInterpretation(target); | ||
27 | return activationTuple -> { | ||
28 | int arity = argumentIndices.length; | ||
29 | var arguments = new int[arity]; | ||
30 | for (int i = 0; i < arity; i++) { | ||
31 | arguments[i] = activationTuple.get(argumentIndices[i]); | ||
32 | } | ||
33 | return targetInterpretation.merge(Tuple.of(arguments), value); | ||
34 | }; | ||
35 | } | ||
36 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java new file mode 100644 index 00000000..8a812518 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java | |||
@@ -0,0 +1,38 @@ | |||
1 | package tools.refinery.store.reasoning.rule; | ||
2 | |||
3 | import tools.refinery.store.model.Model; | ||
4 | import tools.refinery.store.query.Dnf; | ||
5 | |||
6 | import java.util.ArrayList; | ||
7 | import java.util.HashSet; | ||
8 | import java.util.List; | ||
9 | |||
10 | public record Rule(Dnf precondition, List<RuleAction> actions) { | ||
11 | public Rule { | ||
12 | var parameterSet = new HashSet<>(precondition.getParameters()); | ||
13 | for (var action : actions) { | ||
14 | for (var argument : action.arguments()) { | ||
15 | if (!parameterSet.contains(argument)) { | ||
16 | throw new IllegalArgumentException( | ||
17 | "Argument %s of action %s does not appear in the parameter list %s of %s" | ||
18 | .formatted(argument, action, precondition.getParameters(), precondition.name())); | ||
19 | } | ||
20 | } | ||
21 | } | ||
22 | } | ||
23 | |||
24 | public RuleExecutor createExecutor(Model model) { | ||
25 | var parameters = precondition.getParameters(); | ||
26 | var actionExecutors = new ArrayList<RuleActionExecutor>(actions.size()); | ||
27 | for (var action : actions) { | ||
28 | var arguments = action.arguments(); | ||
29 | int arity = arguments.size(); | ||
30 | var argumentIndices = new int[arity]; | ||
31 | for (int i = 0; i < arity; i++) { | ||
32 | argumentIndices[i] = parameters.indexOf(arguments.get(i)); | ||
33 | } | ||
34 | actionExecutors.add(action.createExecutor(argumentIndices, model)); | ||
35 | } | ||
36 | return new RuleExecutor(this, model, actionExecutors); | ||
37 | } | ||
38 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java new file mode 100644 index 00000000..bf980759 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java | |||
@@ -0,0 +1,12 @@ | |||
1 | package tools.refinery.store.reasoning.rule; | ||
2 | |||
3 | import tools.refinery.store.model.Model; | ||
4 | import tools.refinery.store.query.Variable; | ||
5 | |||
6 | import java.util.List; | ||
7 | |||
8 | public interface RuleAction { | ||
9 | List<Variable> arguments(); | ||
10 | |||
11 | RuleActionExecutor createExecutor(int[] argumentIndices, Model model); | ||
12 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleActionExecutor.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleActionExecutor.java new file mode 100644 index 00000000..80bfa6f8 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleActionExecutor.java | |||
@@ -0,0 +1,9 @@ | |||
1 | package tools.refinery.store.reasoning.rule; | ||
2 | |||
3 | import tools.refinery.store.reasoning.MergeResult; | ||
4 | import tools.refinery.store.tuple.TupleLike; | ||
5 | |||
6 | @FunctionalInterface | ||
7 | public interface RuleActionExecutor { | ||
8 | MergeResult execute(TupleLike activationTuple); | ||
9 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleExecutor.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleExecutor.java new file mode 100644 index 00000000..1e5322b4 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleExecutor.java | |||
@@ -0,0 +1,34 @@ | |||
1 | package tools.refinery.store.reasoning.rule; | ||
2 | |||
3 | import tools.refinery.store.reasoning.MergeResult; | ||
4 | import tools.refinery.store.model.Model; | ||
5 | import tools.refinery.store.tuple.TupleLike; | ||
6 | |||
7 | import java.util.List; | ||
8 | |||
9 | public final class RuleExecutor { | ||
10 | private final Rule rule; | ||
11 | private final Model model; | ||
12 | private final List<RuleActionExecutor> actionExecutors; | ||
13 | |||
14 | RuleExecutor(Rule rule, Model model, List<RuleActionExecutor> actionExecutors) { | ||
15 | this.rule = rule; | ||
16 | this.model = model; | ||
17 | this.actionExecutors = actionExecutors; | ||
18 | } | ||
19 | |||
20 | public Rule getRule() { | ||
21 | return rule; | ||
22 | } | ||
23 | |||
24 | public Model getModel() { | ||
25 | return model; | ||
26 | } | ||
27 | public MergeResult execute(TupleLike activationTuple) { | ||
28 | MergeResult mergeResult = MergeResult.UNCHANGED; | ||
29 | for (var actionExecutor : actionExecutors) { | ||
30 | mergeResult = mergeResult.andAlso(actionExecutor.execute(activationTuple)); | ||
31 | } | ||
32 | return mergeResult; | ||
33 | } | ||
34 | } | ||
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 new file mode 100644 index 00000000..7909a7e1 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java | |||
@@ -0,0 +1,159 @@ | |||
1 | package tools.refinery.store.reasoning.translator; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
4 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
5 | import tools.refinery.store.query.Variable; | ||
6 | import tools.refinery.store.query.literal.Literal; | ||
7 | import tools.refinery.store.query.substitution.Substitutions; | ||
8 | |||
9 | import java.util.*; | ||
10 | |||
11 | public final class Advice { | ||
12 | private final AnyPartialSymbol source; | ||
13 | private final PartialRelation target; | ||
14 | private final AdviceSlot slot; | ||
15 | private final boolean mandatory; | ||
16 | private final List<Variable> parameters; | ||
17 | private final List<Literal> literals; | ||
18 | private boolean processed; | ||
19 | |||
20 | public Advice(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot, boolean mandatory, List<Variable> parameters, List<Literal> literals) { | ||
21 | if (mandatory && !slot.isMonotonic()) { | ||
22 | throw new IllegalArgumentException("Only monotonic advice can be mandatory"); | ||
23 | } | ||
24 | this.source = source; | ||
25 | this.target = target; | ||
26 | this.slot = slot; | ||
27 | this.mandatory = mandatory; | ||
28 | checkArity(parameters); | ||
29 | this.parameters = parameters; | ||
30 | this.literals = literals; | ||
31 | } | ||
32 | |||
33 | public AnyPartialSymbol source() { | ||
34 | return source; | ||
35 | } | ||
36 | |||
37 | public PartialRelation target() { | ||
38 | return target; | ||
39 | } | ||
40 | |||
41 | public AdviceSlot slot() { | ||
42 | return slot; | ||
43 | } | ||
44 | |||
45 | public boolean mandatory() { | ||
46 | return mandatory; | ||
47 | } | ||
48 | |||
49 | public List<Variable> parameters() { | ||
50 | return parameters; | ||
51 | } | ||
52 | |||
53 | public List<Literal> literals() { | ||
54 | return literals; | ||
55 | } | ||
56 | |||
57 | public boolean processed() { | ||
58 | return processed; | ||
59 | } | ||
60 | |||
61 | public List<Literal> substitute(List<Variable> substituteParameters) { | ||
62 | checkArity(substituteParameters); | ||
63 | markProcessed(); | ||
64 | int arity = parameters.size(); | ||
65 | var variableMap = new HashMap<Variable, Variable>(arity); | ||
66 | for (int i = 0; i < arity; i++) { | ||
67 | variableMap.put(parameters.get(i), substituteParameters.get(i)); | ||
68 | } | ||
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 = Substitutions.renewing(variableMap); | ||
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 new file mode 100644 index 00000000..f3bd9c5e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java | |||
@@ -0,0 +1,25 @@ | |||
1 | package tools.refinery.store.reasoning.translator; | ||
2 | |||
3 | import tools.refinery.store.representation.TruthValue; | ||
4 | |||
5 | public enum AdviceSlot { | ||
6 | EXTEND_MUST(true), | ||
7 | |||
8 | RESTRICT_MAY(true), | ||
9 | |||
10 | /** | ||
11 | * Same as {@link #RESTRICT_MAY}, but only active if the value of the relation is not {@link TruthValue#TRUE} or | ||
12 | * {@link TruthValue#ERROR}. | ||
13 | */ | ||
14 | RESTRICT_NEW(false); | ||
15 | |||
16 | private final boolean monotonic; | ||
17 | |||
18 | AdviceSlot(boolean monotonic) { | ||
19 | this.monotonic = monotonic; | ||
20 | } | ||
21 | |||
22 | public boolean isMonotonic() { | ||
23 | return monotonic; | ||
24 | } | ||
25 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Seed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Seed.java new file mode 100644 index 00000000..779eadbe --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Seed.java | |||
@@ -0,0 +1,12 @@ | |||
1 | package tools.refinery.store.reasoning.translator; | ||
2 | |||
3 | import tools.refinery.store.map.Cursor; | ||
4 | import tools.refinery.store.tuple.Tuple; | ||
5 | |||
6 | public interface Seed<T> { | ||
7 | int arity(); | ||
8 | |||
9 | T get(Tuple key); | ||
10 | |||
11 | Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount); | ||
12 | } | ||
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 new file mode 100644 index 00000000..e45d20c8 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java | |||
@@ -0,0 +1,48 @@ | |||
1 | package tools.refinery.store.reasoning.translator; | ||
2 | |||
3 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
4 | import tools.refinery.store.model.Model; | ||
5 | import tools.refinery.store.model.ModelStoreBuilder; | ||
6 | import tools.refinery.store.reasoning.AnyPartialInterpretation; | ||
7 | import tools.refinery.store.reasoning.literal.Modality; | ||
8 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
9 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
10 | import tools.refinery.store.query.Variable; | ||
11 | import tools.refinery.store.query.literal.CallPolarity; | ||
12 | import tools.refinery.store.query.literal.Literal; | ||
13 | |||
14 | import java.util.Collection; | ||
15 | import java.util.List; | ||
16 | import java.util.Map; | ||
17 | |||
18 | public abstract class TranslationUnit { | ||
19 | private ReasoningBuilder reasoningBuilder; | ||
20 | |||
21 | protected ReasoningBuilder getPartialInterpretationBuilder() { | ||
22 | return reasoningBuilder; | ||
23 | } | ||
24 | |||
25 | public void setPartialInterpretationBuilder(ReasoningBuilder reasoningBuilder) { | ||
26 | this.reasoningBuilder = reasoningBuilder; | ||
27 | } | ||
28 | |||
29 | protected ModelStoreBuilder getModelStoreBuilder() { | ||
30 | return reasoningBuilder.getStoreBuilder(); | ||
31 | } | ||
32 | |||
33 | public abstract Collection<AnyPartialSymbol> getTranslatedPartialSymbols(); | ||
34 | |||
35 | public Collection<Advice> computeAdvices() { | ||
36 | // No advices to give by default. | ||
37 | return List.of(); | ||
38 | } | ||
39 | |||
40 | public abstract void configure(Collection<Advice> advices); | ||
41 | |||
42 | public abstract List<Literal> call(CallPolarity polarity, Modality modality, PartialRelation target, | ||
43 | List<Variable> arguments); | ||
44 | |||
45 | public abstract Map<AnyPartialSymbol, AnyPartialInterpretation> createPartialInterpretations(Model model); | ||
46 | |||
47 | public abstract void initializeModel(Model model, int nodeCount); | ||
48 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java new file mode 100644 index 00000000..1b8d7cc9 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java | |||
@@ -0,0 +1,6 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
4 | |||
5 | record EliminatedType(PartialRelation replacement) implements TypeAnalysisResult { | ||
6 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/ExtendedTypeInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/ExtendedTypeInfo.java new file mode 100644 index 00000000..43b8e1dd --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/ExtendedTypeInfo.java | |||
@@ -0,0 +1,101 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import org.jetbrains.annotations.NotNull; | ||
4 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
5 | |||
6 | import java.util.HashSet; | ||
7 | import java.util.LinkedHashSet; | ||
8 | import java.util.Objects; | ||
9 | import java.util.Set; | ||
10 | |||
11 | final class ExtendedTypeInfo implements Comparable<ExtendedTypeInfo> { | ||
12 | private final int index; | ||
13 | private final PartialRelation type; | ||
14 | private final TypeInfo typeInfo; | ||
15 | private final Set<PartialRelation> allSubtypes = new LinkedHashSet<>(); | ||
16 | private final Set<PartialRelation> allSupertypes; | ||
17 | private final Set<PartialRelation> concreteSubtypesAndSelf = new LinkedHashSet<>(); | ||
18 | private Set<PartialRelation> directSubtypes; | ||
19 | private final Set<PartialRelation> unsortedDirectSupertypes = new HashSet<>(); | ||
20 | |||
21 | public ExtendedTypeInfo(int index, PartialRelation type, TypeInfo typeInfo) { | ||
22 | this.index = index; | ||
23 | this.type = type; | ||
24 | this.typeInfo = typeInfo; | ||
25 | this.allSupertypes = new LinkedHashSet<>(typeInfo.supertypes()); | ||
26 | } | ||
27 | |||
28 | public PartialRelation getType() { | ||
29 | return type; | ||
30 | } | ||
31 | |||
32 | public TypeInfo getTypeInfo() { | ||
33 | return typeInfo; | ||
34 | } | ||
35 | |||
36 | public boolean isAbstractType() { | ||
37 | return getTypeInfo().abstractType(); | ||
38 | } | ||
39 | |||
40 | public Set<PartialRelation> getAllSubtypes() { | ||
41 | return allSubtypes; | ||
42 | } | ||
43 | |||
44 | public Set<PartialRelation> getAllSupertypes() { | ||
45 | return allSupertypes; | ||
46 | } | ||
47 | |||
48 | public Set<PartialRelation> getAllSupertypesAndSelf() { | ||
49 | var allSubtypesAndSelf = new HashSet<PartialRelation>(allSupertypes.size() + 1); | ||
50 | addMust(allSubtypesAndSelf); | ||
51 | return allSubtypesAndSelf; | ||
52 | } | ||
53 | |||
54 | public Set<PartialRelation> getConcreteSubtypesAndSelf() { | ||
55 | return concreteSubtypesAndSelf; | ||
56 | } | ||
57 | |||
58 | public Set<PartialRelation> getDirectSubtypes() { | ||
59 | return directSubtypes; | ||
60 | } | ||
61 | |||
62 | public Set<PartialRelation> getUnsortedDirectSupertypes() { | ||
63 | return unsortedDirectSupertypes; | ||
64 | } | ||
65 | |||
66 | public void setDirectSubtypes(Set<PartialRelation> directSubtypes) { | ||
67 | this.directSubtypes = directSubtypes; | ||
68 | } | ||
69 | |||
70 | public boolean allowsAllConcreteTypes(Set<PartialRelation> concreteTypes) { | ||
71 | for (var concreteType : concreteTypes) { | ||
72 | if (!concreteSubtypesAndSelf.contains(concreteType)) { | ||
73 | return false; | ||
74 | } | ||
75 | } | ||
76 | return true; | ||
77 | } | ||
78 | |||
79 | public void addMust(Set<PartialRelation> mustTypes) { | ||
80 | mustTypes.add(type); | ||
81 | mustTypes.addAll(allSupertypes); | ||
82 | } | ||
83 | |||
84 | @Override | ||
85 | public int compareTo(@NotNull ExtendedTypeInfo extendedTypeInfo) { | ||
86 | return Integer.compare(index, extendedTypeInfo.index); | ||
87 | } | ||
88 | |||
89 | @Override | ||
90 | public boolean equals(Object o) { | ||
91 | if (this == o) return true; | ||
92 | if (o == null || getClass() != o.getClass()) return false; | ||
93 | ExtendedTypeInfo that = (ExtendedTypeInfo) o; | ||
94 | return index == that.index; | ||
95 | } | ||
96 | |||
97 | @Override | ||
98 | public int hashCode() { | ||
99 | return Objects.hash(index); | ||
100 | } | ||
101 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeRelationView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeRelationView.java new file mode 100644 index 00000000..12c37c86 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeRelationView.java | |||
@@ -0,0 +1,19 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
4 | import tools.refinery.store.query.view.TuplePreservingRelationView; | ||
5 | import tools.refinery.store.tuple.Tuple; | ||
6 | |||
7 | class InferredMayTypeRelationView extends TuplePreservingRelationView<InferredType> { | ||
8 | private final PartialRelation type; | ||
9 | |||
10 | InferredMayTypeRelationView(PartialRelation type) { | ||
11 | super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#may".formatted(type)); | ||
12 | this.type = type; | ||
13 | } | ||
14 | |||
15 | @Override | ||
16 | public boolean filter(Tuple key, InferredType value) { | ||
17 | return value.mayConcreteTypes().contains(type); | ||
18 | } | ||
19 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeRelationView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeRelationView.java new file mode 100644 index 00000000..975f627e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeRelationView.java | |||
@@ -0,0 +1,19 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
4 | import tools.refinery.store.query.view.TuplePreservingRelationView; | ||
5 | import tools.refinery.store.tuple.Tuple; | ||
6 | |||
7 | class InferredMustTypeRelationView extends TuplePreservingRelationView<InferredType> { | ||
8 | private final PartialRelation type; | ||
9 | |||
10 | InferredMustTypeRelationView(PartialRelation type) { | ||
11 | super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#must".formatted(type)); | ||
12 | this.type = type; | ||
13 | } | ||
14 | |||
15 | @Override | ||
16 | public boolean filter(Tuple key, InferredType value) { | ||
17 | return value.mustTypes().contains(type); | ||
18 | } | ||
19 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java new file mode 100644 index 00000000..a366e262 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java | |||
@@ -0,0 +1,30 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
4 | |||
5 | import java.util.Collections; | ||
6 | import java.util.Set; | ||
7 | |||
8 | record InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes, | ||
9 | PartialRelation currentType) { | ||
10 | public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null); | ||
11 | |||
12 | public InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes, | ||
13 | PartialRelation currentType) { | ||
14 | this.mustTypes = Collections.unmodifiableSet(mustTypes); | ||
15 | this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes); | ||
16 | this.currentType = currentType; | ||
17 | } | ||
18 | |||
19 | public boolean isConsistent() { | ||
20 | return currentType != null || mustTypes.isEmpty(); | ||
21 | } | ||
22 | |||
23 | public boolean isMust(PartialRelation partialRelation) { | ||
24 | return mustTypes.contains(partialRelation); | ||
25 | } | ||
26 | |||
27 | public boolean isMayConcrete(PartialRelation partialRelation) { | ||
28 | return mayConcreteTypes.contains(partialRelation); | ||
29 | } | ||
30 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java new file mode 100644 index 00000000..63dba964 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java | |||
@@ -0,0 +1,136 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
4 | import tools.refinery.store.representation.TruthValue; | ||
5 | |||
6 | import java.util.*; | ||
7 | |||
8 | final class PreservedType implements TypeAnalysisResult { | ||
9 | private final ExtendedTypeInfo extendedTypeInfo; | ||
10 | private final List<PartialRelation> directSubtypes; | ||
11 | private final List<ExtendedTypeInfo> allExternalTypeInfoList; | ||
12 | private final InferredType inferredType; | ||
13 | |||
14 | public PreservedType(ExtendedTypeInfo extendedTypeInfo, List<ExtendedTypeInfo> allExternalTypeInfoList) { | ||
15 | this.extendedTypeInfo = extendedTypeInfo; | ||
16 | directSubtypes = List.copyOf(extendedTypeInfo.getDirectSubtypes()); | ||
17 | this.allExternalTypeInfoList = allExternalTypeInfoList; | ||
18 | inferredType = propagateMust(extendedTypeInfo.getAllSupertypesAndSelf(), | ||
19 | extendedTypeInfo.getConcreteSubtypesAndSelf()); | ||
20 | } | ||
21 | |||
22 | public PartialRelation type() { | ||
23 | return extendedTypeInfo.getType(); | ||
24 | } | ||
25 | |||
26 | public List<PartialRelation> getDirectSubtypes() { | ||
27 | return directSubtypes; | ||
28 | } | ||
29 | |||
30 | public boolean isAbstractType() { | ||
31 | return extendedTypeInfo.isAbstractType(); | ||
32 | } | ||
33 | |||
34 | public boolean isVacuous() { | ||
35 | return isAbstractType() && directSubtypes.isEmpty(); | ||
36 | } | ||
37 | |||
38 | public InferredType asInferredType() { | ||
39 | return inferredType; | ||
40 | } | ||
41 | |||
42 | public InferredType merge(InferredType inferredType, TruthValue value) { | ||
43 | return switch (value) { | ||
44 | case UNKNOWN -> inferredType; | ||
45 | case TRUE -> addMust(inferredType); | ||
46 | case FALSE -> removeMay(inferredType); | ||
47 | case ERROR -> addError(inferredType); | ||
48 | }; | ||
49 | } | ||
50 | |||
51 | private InferredType addMust(InferredType inferredType) { | ||
52 | var originalMustTypes = inferredType.mustTypes(); | ||
53 | if (originalMustTypes.contains(type())) { | ||
54 | return inferredType; | ||
55 | } | ||
56 | var mustTypes = new HashSet<>(originalMustTypes); | ||
57 | extendedTypeInfo.addMust(mustTypes); | ||
58 | var originalMayConcreteTypes = inferredType.mayConcreteTypes(); | ||
59 | var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes); | ||
60 | Set<PartialRelation> mayConcreteTypesResult; | ||
61 | if (mayConcreteTypes.retainAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) { | ||
62 | mayConcreteTypesResult = mayConcreteTypes; | ||
63 | } else { | ||
64 | mayConcreteTypesResult = originalMayConcreteTypes; | ||
65 | } | ||
66 | return propagateMust(mustTypes, mayConcreteTypesResult); | ||
67 | } | ||
68 | |||
69 | private InferredType removeMay(InferredType inferredType) { | ||
70 | var originalMayConcreteTypes = inferredType.mayConcreteTypes(); | ||
71 | var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes); | ||
72 | if (!mayConcreteTypes.removeAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) { | ||
73 | return inferredType; | ||
74 | } | ||
75 | return propagateMust(inferredType.mustTypes(), mayConcreteTypes); | ||
76 | } | ||
77 | |||
78 | private InferredType addError(InferredType inferredType) { | ||
79 | var originalMustTypes = inferredType.mustTypes(); | ||
80 | if (originalMustTypes.contains(type())) { | ||
81 | if (inferredType.mayConcreteTypes().isEmpty()) { | ||
82 | return inferredType; | ||
83 | } | ||
84 | return new InferredType(originalMustTypes, Set.of(), null); | ||
85 | } | ||
86 | var mustTypes = new HashSet<>(originalMustTypes); | ||
87 | extendedTypeInfo.addMust(mustTypes); | ||
88 | return new InferredType(mustTypes, Set.of(), null); | ||
89 | } | ||
90 | |||
91 | private InferredType propagateMust(Set<PartialRelation> originalMustTypes, | ||
92 | Set<PartialRelation> mayConcreteTypes) { | ||
93 | // It is possible that there is not type at all, do not force one by propagation. | ||
94 | var maybeUntyped = originalMustTypes.isEmpty(); | ||
95 | // Para-consistent case, do not propagate must types to avoid logical explosion. | ||
96 | var paraConsistentOrSurelyUntyped = mayConcreteTypes.isEmpty(); | ||
97 | if (maybeUntyped || paraConsistentOrSurelyUntyped) { | ||
98 | return new InferredType(originalMustTypes, mayConcreteTypes, null); | ||
99 | } | ||
100 | var currentType = computeCurrentType(mayConcreteTypes); | ||
101 | var mustTypes = new HashSet<>(originalMustTypes); | ||
102 | boolean changed = false; | ||
103 | for (var newMustExtendedTypeInfo : allExternalTypeInfoList) { | ||
104 | var newMustType = newMustExtendedTypeInfo.getType(); | ||
105 | if (mustTypes.contains(newMustType)) { | ||
106 | continue; | ||
107 | } | ||
108 | if (newMustExtendedTypeInfo.allowsAllConcreteTypes(mayConcreteTypes)) { | ||
109 | newMustExtendedTypeInfo.addMust(mustTypes); | ||
110 | changed = true; | ||
111 | } | ||
112 | } | ||
113 | if (!changed) { | ||
114 | return new InferredType(originalMustTypes, mayConcreteTypes, currentType); | ||
115 | } | ||
116 | return new InferredType(mustTypes, mayConcreteTypes, currentType); | ||
117 | } | ||
118 | |||
119 | /** | ||
120 | * Returns a concrete type that is allowed by a (consistent, i.e., nonempty) set of <b>may</b> concrete types. | ||
121 | * | ||
122 | * @param mayConcreteTypes The set of allowed concrete types. Must not be empty. | ||
123 | * @return The first concrete type that is allowed by {@code matConcreteTypes}. | ||
124 | */ | ||
125 | private PartialRelation computeCurrentType(Set<PartialRelation> mayConcreteTypes) { | ||
126 | for (var concreteExtendedTypeInfo : allExternalTypeInfoList) { | ||
127 | var concreteType = concreteExtendedTypeInfo.getType(); | ||
128 | if (!concreteExtendedTypeInfo.isAbstractType() && mayConcreteTypes.contains(concreteType)) { | ||
129 | return concreteType; | ||
130 | } | ||
131 | } | ||
132 | // We have already filtered out the para-consistent case in {@link #propagateMust(Set<PartialRelation>, | ||
133 | // Set<PartialRelation>}. | ||
134 | throw new AssertionError("No concrete type in %s".formatted(mayConcreteTypes)); | ||
135 | } | ||
136 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java new file mode 100644 index 00000000..4f915108 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java | |||
@@ -0,0 +1,4 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | sealed interface TypeAnalysisResult permits EliminatedType, PreservedType { | ||
4 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzer.java new file mode 100644 index 00000000..62f8e750 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzer.java | |||
@@ -0,0 +1,202 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
4 | |||
5 | import java.util.*; | ||
6 | |||
7 | class TypeAnalyzer { | ||
8 | private final Map<PartialRelation, ExtendedTypeInfo> extendedTypeInfoMap; | ||
9 | private final Map<PartialRelation, PartialRelation> replacements = new LinkedHashMap<>(); | ||
10 | private final InferredType unknownType; | ||
11 | private final Map<PartialRelation, TypeAnalysisResult> analysisResults; | ||
12 | |||
13 | public TypeAnalyzer(Map<PartialRelation, TypeInfo> typeInfoMap) { | ||
14 | int size = typeInfoMap.size(); | ||
15 | extendedTypeInfoMap = new LinkedHashMap<>(size); | ||
16 | var concreteTypes = new LinkedHashSet<PartialRelation>(); | ||
17 | int index = 0; | ||
18 | for (var entry : typeInfoMap.entrySet()) { | ||
19 | var type = entry.getKey(); | ||
20 | var typeInfo = entry.getValue(); | ||
21 | extendedTypeInfoMap.put(type, new ExtendedTypeInfo(index, type, typeInfo)); | ||
22 | if (!typeInfo.abstractType()) { | ||
23 | concreteTypes.add(type); | ||
24 | } | ||
25 | index++; | ||
26 | } | ||
27 | unknownType = new InferredType(Set.of(), concreteTypes, null); | ||
28 | computeAllSupertypes(); | ||
29 | computeAllAndConcreteSubtypes(); | ||
30 | computeDirectSubtypes(); | ||
31 | eliminateTrivialSupertypes(); | ||
32 | analysisResults = computeAnalysisResults(); | ||
33 | } | ||
34 | |||
35 | public InferredType getUnknownType() { | ||
36 | return unknownType; | ||
37 | } | ||
38 | |||
39 | public Map<PartialRelation, TypeAnalysisResult> getAnalysisResults() { | ||
40 | return analysisResults; | ||
41 | } | ||
42 | |||
43 | private void computeAllSupertypes() { | ||
44 | boolean changed; | ||
45 | do { | ||
46 | changed = false; | ||
47 | for (var extendedTypeInfo : extendedTypeInfoMap.values()) { | ||
48 | var found = new HashSet<PartialRelation>(); | ||
49 | var allSupertypes = extendedTypeInfo.getAllSupertypes(); | ||
50 | for (var supertype : allSupertypes) { | ||
51 | found.addAll(extendedTypeInfoMap.get(supertype).getAllSupertypes()); | ||
52 | } | ||
53 | if (allSupertypes.addAll(found)) { | ||
54 | changed = true; | ||
55 | } | ||
56 | } | ||
57 | } while (changed); | ||
58 | } | ||
59 | |||
60 | private void computeAllAndConcreteSubtypes() { | ||
61 | for (var extendedTypeInfo : extendedTypeInfoMap.values()) { | ||
62 | var type = extendedTypeInfo.getType(); | ||
63 | if (!extendedTypeInfo.isAbstractType()) { | ||
64 | extendedTypeInfo.getConcreteSubtypesAndSelf().add(type); | ||
65 | } | ||
66 | for (var supertype : extendedTypeInfo.getAllSupertypes()) { | ||
67 | if (type.equals(supertype)) { | ||
68 | throw new IllegalArgumentException("%s cannot be a supertype of itself".formatted(type)); | ||
69 | } | ||
70 | var supertypeInfo = extendedTypeInfoMap.get(supertype); | ||
71 | supertypeInfo.getAllSubtypes().add(type); | ||
72 | if (!extendedTypeInfo.isAbstractType()) { | ||
73 | supertypeInfo.getConcreteSubtypesAndSelf().add(type); | ||
74 | } | ||
75 | } | ||
76 | } | ||
77 | } | ||
78 | |||
79 | private void computeDirectSubtypes() { | ||
80 | for (var extendedTypeInfo : extendedTypeInfoMap.values()) { | ||
81 | var allSubtypes = extendedTypeInfo.getAllSubtypes(); | ||
82 | var directSubtypes = new LinkedHashSet<>(allSubtypes); | ||
83 | var indirectSubtypes = new LinkedHashSet<PartialRelation>(allSubtypes.size()); | ||
84 | for (var subtype : allSubtypes) { | ||
85 | indirectSubtypes.addAll(extendedTypeInfoMap.get(subtype).getAllSubtypes()); | ||
86 | } | ||
87 | directSubtypes.removeAll(indirectSubtypes); | ||
88 | extendedTypeInfo.setDirectSubtypes(directSubtypes); | ||
89 | } | ||
90 | } | ||
91 | |||
92 | private void eliminateTrivialSupertypes() { | ||
93 | boolean changed; | ||
94 | do { | ||
95 | var toRemove = new ArrayList<PartialRelation>(); | ||
96 | for (var entry : extendedTypeInfoMap.entrySet()) { | ||
97 | var extendedTypeInfo = entry.getValue(); | ||
98 | boolean isAbstract = extendedTypeInfo.isAbstractType(); | ||
99 | // Do not eliminate abstract types with 0 subtypes, because they can be used para-consistently, i.e., | ||
100 | // an object determined to <b>must</b> have an abstract type with 0 subtypes <b>may not</b> ever exist. | ||
101 | boolean hasSingleDirectSubtype = extendedTypeInfo.getDirectSubtypes().size() == 1; | ||
102 | if (isAbstract && hasSingleDirectSubtype) { | ||
103 | toRemove.add(entry.getKey()); | ||
104 | } | ||
105 | } | ||
106 | toRemove.forEach(this::removeTrivialType); | ||
107 | changed = !toRemove.isEmpty(); | ||
108 | } while (changed); | ||
109 | } | ||
110 | |||
111 | private void removeTrivialType(PartialRelation trivialType) { | ||
112 | var extendedTypeInfo = extendedTypeInfoMap.get(trivialType); | ||
113 | var iterator = extendedTypeInfo.getDirectSubtypes().iterator(); | ||
114 | if (!iterator.hasNext()) { | ||
115 | throw new AssertionError("Expected trivial supertype %s to have a direct subtype" | ||
116 | .formatted(trivialType)); | ||
117 | } | ||
118 | PartialRelation replacement = setReplacement(trivialType, iterator.next()); | ||
119 | if (iterator.hasNext()) { | ||
120 | throw new AssertionError("Expected trivial supertype %s to have at most 1 direct subtype" | ||
121 | .formatted(trivialType)); | ||
122 | } | ||
123 | replacements.put(trivialType, replacement); | ||
124 | for (var supertype : extendedTypeInfo.getAllSupertypes()) { | ||
125 | var extendedSupertypeInfo = extendedTypeInfoMap.get(supertype); | ||
126 | if (!extendedSupertypeInfo.getAllSubtypes().remove(trivialType)) { | ||
127 | throw new AssertionError("Expected %s to be subtype of %s".formatted(trivialType, supertype)); | ||
128 | } | ||
129 | var directSubtypes = extendedSupertypeInfo.getDirectSubtypes(); | ||
130 | if (directSubtypes.remove(trivialType)) { | ||
131 | directSubtypes.add(replacement); | ||
132 | } | ||
133 | } | ||
134 | for (var subtype : extendedTypeInfo.getAllSubtypes()) { | ||
135 | var extendedSubtypeInfo = extendedTypeInfoMap.get(subtype); | ||
136 | if (!extendedSubtypeInfo.getAllSupertypes().remove(trivialType)) { | ||
137 | throw new AssertionError("Expected %s to be supertype of %s".formatted(trivialType, subtype)); | ||
138 | } | ||
139 | } | ||
140 | extendedTypeInfoMap.remove(trivialType); | ||
141 | } | ||
142 | |||
143 | private PartialRelation setReplacement(PartialRelation trivialRelation, PartialRelation replacement) { | ||
144 | if (replacement == null) { | ||
145 | return trivialRelation; | ||
146 | } | ||
147 | var resolved = setReplacement(replacement, replacements.get(replacement)); | ||
148 | replacements.put(trivialRelation, resolved); | ||
149 | return resolved; | ||
150 | } | ||
151 | |||
152 | private Map<PartialRelation, TypeAnalysisResult> computeAnalysisResults() { | ||
153 | var allExtendedTypeInfoList = sortTypes(); | ||
154 | var results = new LinkedHashMap<PartialRelation, TypeAnalysisResult>( | ||
155 | allExtendedTypeInfoList.size() + replacements.size()); | ||
156 | for (var extendedTypeInfo : allExtendedTypeInfoList) { | ||
157 | var type = extendedTypeInfo.getType(); | ||
158 | results.put(type, new PreservedType(extendedTypeInfo, allExtendedTypeInfoList)); | ||
159 | } | ||
160 | for (var entry : replacements.entrySet()) { | ||
161 | var type = entry.getKey(); | ||
162 | results.put(type, new EliminatedType(entry.getValue())); | ||
163 | } | ||
164 | return Collections.unmodifiableMap(results); | ||
165 | } | ||
166 | |||
167 | private List<ExtendedTypeInfo> sortTypes() { | ||
168 | // Invert {@code directSubtypes} to keep track of the out-degree of types. | ||
169 | for (var extendedTypeInfo : extendedTypeInfoMap.values()) { | ||
170 | for (var directSubtype : extendedTypeInfo.getDirectSubtypes()) { | ||
171 | var extendedDirectSubtypeInfo = extendedTypeInfoMap.get(directSubtype); | ||
172 | extendedDirectSubtypeInfo.getUnsortedDirectSupertypes().add(extendedTypeInfo.getType()); | ||
173 | } | ||
174 | } | ||
175 | // Build a <i>inverse</i> topological order ({@code extends} edges always points to earlier nodes in the order, | ||
176 | // breaking ties according to the original order ({@link ExtendedTypeInfo#index}) to form a 'stable' sort. | ||
177 | // See, e.g., https://stackoverflow.com/a/11236027. | ||
178 | var priorityQueue = new PriorityQueue<ExtendedTypeInfo>(); | ||
179 | for (var extendedTypeInfo : extendedTypeInfoMap.values()) { | ||
180 | if (extendedTypeInfo.getUnsortedDirectSupertypes().isEmpty()) { | ||
181 | priorityQueue.add(extendedTypeInfo); | ||
182 | } | ||
183 | } | ||
184 | var sorted = new ArrayList<ExtendedTypeInfo>(extendedTypeInfoMap.size()); | ||
185 | while (!priorityQueue.isEmpty()) { | ||
186 | var extendedTypeInfo = priorityQueue.remove(); | ||
187 | sorted.add(extendedTypeInfo); | ||
188 | for (var directSubtype : extendedTypeInfo.getDirectSubtypes()) { | ||
189 | var extendedDirectSubtypeInfo = extendedTypeInfoMap.get(directSubtype); | ||
190 | var unsortedDirectSupertypes = extendedDirectSubtypeInfo.getUnsortedDirectSupertypes(); | ||
191 | if (!unsortedDirectSupertypes.remove(extendedTypeInfo.getType())) { | ||
192 | throw new AssertionError("Expected %s to be a direct supertype of %s" | ||
193 | .formatted(extendedTypeInfo.getType(), directSubtype)); | ||
194 | } | ||
195 | if (unsortedDirectSupertypes.isEmpty()) { | ||
196 | priorityQueue.add(extendedDirectSubtypeInfo); | ||
197 | } | ||
198 | } | ||
199 | } | ||
200 | return Collections.unmodifiableList(sorted); | ||
201 | } | ||
202 | } | ||
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 new file mode 100644 index 00000000..c800b4cd --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java | |||
@@ -0,0 +1,52 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import tools.refinery.store.reasoning.AnyPartialInterpretation; | ||
4 | import tools.refinery.store.reasoning.literal.Modality; | ||
5 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
6 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
7 | import tools.refinery.store.reasoning.translator.Advice; | ||
8 | import tools.refinery.store.reasoning.translator.TranslationUnit; | ||
9 | import tools.refinery.store.model.Model; | ||
10 | import tools.refinery.store.query.Variable; | ||
11 | import tools.refinery.store.query.literal.CallPolarity; | ||
12 | import tools.refinery.store.query.literal.Literal; | ||
13 | import tools.refinery.store.representation.Symbol; | ||
14 | |||
15 | import java.util.*; | ||
16 | |||
17 | public class TypeHierarchyTranslationUnit extends TranslationUnit { | ||
18 | static final Symbol<InferredType> INFERRED_TYPE_SYMBOL = new Symbol<>("inferredType", 1, | ||
19 | InferredType.class, InferredType.UNTYPED); | ||
20 | |||
21 | private final TypeAnalyzer typeAnalyzer; | ||
22 | |||
23 | public TypeHierarchyTranslationUnit(Map<PartialRelation, TypeInfo> typeInfoMap) { | ||
24 | typeAnalyzer = new TypeAnalyzer(typeInfoMap); | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public Collection<AnyPartialSymbol> getTranslatedPartialSymbols() { | ||
29 | return null; | ||
30 | } | ||
31 | |||
32 | @Override | ||
33 | public void configure(Collection<Advice> advices) { | ||
34 | |||
35 | } | ||
36 | |||
37 | @Override | ||
38 | public List<Literal> call(CallPolarity polarity, Modality modality, PartialRelation target, | ||
39 | List<Variable> arguments) { | ||
40 | return null; | ||
41 | } | ||
42 | |||
43 | @Override | ||
44 | public Map<AnyPartialSymbol, AnyPartialInterpretation> createPartialInterpretations(Model model) { | ||
45 | return null; | ||
46 | } | ||
47 | |||
48 | @Override | ||
49 | public void initializeModel(Model model, int nodeCount) { | ||
50 | |||
51 | } | ||
52 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java new file mode 100644 index 00000000..313df4df --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java | |||
@@ -0,0 +1,46 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
4 | |||
5 | import java.util.*; | ||
6 | |||
7 | public record TypeInfo(Collection<PartialRelation> supertypes, boolean abstractType) { | ||
8 | public static Builder builder() { | ||
9 | return new Builder(); | ||
10 | } | ||
11 | |||
12 | public static class Builder { | ||
13 | private final Set<PartialRelation> supertypes = new LinkedHashSet<>(); | ||
14 | private boolean abstractType; | ||
15 | |||
16 | private Builder() { | ||
17 | } | ||
18 | |||
19 | public Builder supertypes(Collection<PartialRelation> supertypes) { | ||
20 | this.supertypes.addAll(supertypes); | ||
21 | return this; | ||
22 | } | ||
23 | |||
24 | public Builder supertypes(PartialRelation... supertypes) { | ||
25 | return supertypes(List.of(supertypes)); | ||
26 | } | ||
27 | |||
28 | public Builder supertype(PartialRelation supertype) { | ||
29 | supertypes.add(supertype); | ||
30 | return this; | ||
31 | } | ||
32 | |||
33 | public Builder abstractType(boolean abstractType) { | ||
34 | this.abstractType = abstractType; | ||
35 | return this; | ||
36 | } | ||
37 | |||
38 | public Builder abstractType() { | ||
39 | return abstractType(true); | ||
40 | } | ||
41 | |||
42 | public TypeInfo build() { | ||
43 | return new TypeInfo(Collections.unmodifiableSet(supertypes), abstractType); | ||
44 | } | ||
45 | } | ||
46 | } | ||
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeTest.java new file mode 100644 index 00000000..a8df2312 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeTest.java | |||
@@ -0,0 +1,32 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import org.junit.jupiter.api.Test; | ||
4 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
5 | |||
6 | import java.util.Set; | ||
7 | |||
8 | import static org.hamcrest.MatcherAssert.assertThat; | ||
9 | import static org.hamcrest.Matchers.is; | ||
10 | |||
11 | class InferredTypeTest { | ||
12 | private final PartialRelation c1 = new PartialRelation("C1", 1); | ||
13 | private final PartialRelation c2 = new PartialRelation("C2", 1); | ||
14 | |||
15 | @Test | ||
16 | void untypedIsConsistentTest() { | ||
17 | var sut = new InferredType(Set.of(), Set.of(c1, c2), null); | ||
18 | assertThat(sut.isConsistent(), is(true)); | ||
19 | } | ||
20 | |||
21 | @Test | ||
22 | void typedIsConsistentTest() { | ||
23 | var sut = new InferredType(Set.of(c1), Set.of(c1, c2), c1); | ||
24 | assertThat(sut.isConsistent(), is(true)); | ||
25 | } | ||
26 | |||
27 | @Test | ||
28 | void typedIsInconsistentTest() { | ||
29 | var sut = new InferredType(Set.of(c1), Set.of(), null); | ||
30 | assertThat(sut.isConsistent(), is(false)); | ||
31 | } | ||
32 | } | ||
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 new file mode 100644 index 00000000..b2c1ef1b --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java | |||
@@ -0,0 +1,203 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import org.junit.jupiter.api.BeforeEach; | ||
4 | import org.junit.jupiter.api.Test; | ||
5 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
6 | import tools.refinery.store.representation.TruthValue; | ||
7 | |||
8 | import java.util.LinkedHashMap; | ||
9 | import java.util.Set; | ||
10 | |||
11 | import static org.hamcrest.MatcherAssert.assertThat; | ||
12 | import static org.hamcrest.Matchers.is; | ||
13 | import static org.junit.jupiter.api.Assertions.assertAll; | ||
14 | |||
15 | class TypeAnalyzerExampleHierarchyTest { | ||
16 | private final PartialRelation a1 = new PartialRelation("A1", 1); | ||
17 | private final PartialRelation a2 = new PartialRelation("A2", 1); | ||
18 | private final PartialRelation a3 = new PartialRelation("A3", 1); | ||
19 | private final PartialRelation a4 = new PartialRelation("A4", 1); | ||
20 | private final PartialRelation a5 = new PartialRelation("A5", 1); | ||
21 | private final PartialRelation c1 = new PartialRelation("C1", 1); | ||
22 | private final PartialRelation c2 = new PartialRelation("C2", 1); | ||
23 | private final PartialRelation c3 = new PartialRelation("C3", 1); | ||
24 | private final PartialRelation c4 = new PartialRelation("C4", 1); | ||
25 | |||
26 | private TypeAnalyzer sut; | ||
27 | private TypeAnalyzerTester tester; | ||
28 | |||
29 | @BeforeEach | ||
30 | void beforeEach() { | ||
31 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | ||
32 | typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); | ||
33 | typeInfoMap.put(a2, TypeInfo.builder().abstractType().build()); | ||
34 | typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); | ||
35 | typeInfoMap.put(a4, TypeInfo.builder().abstractType().build()); | ||
36 | typeInfoMap.put(a5, TypeInfo.builder().abstractType().build()); | ||
37 | typeInfoMap.put(c1, TypeInfo.builder().supertypes(a1, a4).build()); | ||
38 | typeInfoMap.put(c2, TypeInfo.builder().supertypes(a1, a2, a3, a4).build()); | ||
39 | typeInfoMap.put(c3, TypeInfo.builder().supertype(a3).build()); | ||
40 | typeInfoMap.put(c4, TypeInfo.builder().supertype(a4).build()); | ||
41 | sut = new TypeAnalyzer(typeInfoMap); | ||
42 | tester = new TypeAnalyzerTester(sut); | ||
43 | } | ||
44 | |||
45 | @Test | ||
46 | void analysisResultsTest() { | ||
47 | assertAll( | ||
48 | () -> tester.assertAbstractType(a1, c1, c2), | ||
49 | () -> tester.assertEliminatedType(a2, c2), | ||
50 | () -> tester.assertAbstractType(a3, c2, c3), | ||
51 | () -> tester.assertAbstractType(a4, c1, c2, c4), | ||
52 | () -> tester.assertVacuousType(a5), | ||
53 | () -> tester.assertConcreteType(c1), | ||
54 | () -> tester.assertConcreteType(c2), | ||
55 | () -> tester.assertConcreteType(c3), | ||
56 | () -> tester.assertConcreteType(c4) | ||
57 | ); | ||
58 | } | ||
59 | |||
60 | @Test | ||
61 | void inferredTypesTest() { | ||
62 | assertAll( | ||
63 | () -> assertThat(sut.getUnknownType(), is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))), | ||
64 | () -> assertThat(tester.getInferredType(a1), is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))), | ||
65 | () -> assertThat(tester.getInferredType(a3), is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))), | ||
66 | () -> assertThat(tester.getInferredType(a4), is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))), | ||
67 | () -> assertThat(tester.getInferredType(a5), is(new InferredType(Set.of(a5), Set.of(), null))), | ||
68 | () -> assertThat(tester.getInferredType(c1), is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), | ||
69 | () -> assertThat(tester.getInferredType(c2), | ||
70 | is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))), | ||
71 | () -> assertThat(tester.getInferredType(c3), is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), | ||
72 | () -> assertThat(tester.getInferredType(c4), is(new InferredType(Set.of(a4, c4), Set.of(c4), c4))) | ||
73 | ); | ||
74 | } | ||
75 | |||
76 | @Test | ||
77 | void consistentMustTest() { | ||
78 | var a1Result = tester.getPreservedType(a1); | ||
79 | var a3Result = tester.getPreservedType(a3); | ||
80 | var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2); | ||
81 | assertAll( | ||
82 | () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), is(expected)), | ||
83 | () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), is(expected)), | ||
84 | () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())), | ||
85 | () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())), | ||
86 | () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE), | ||
87 | is(a1Result.asInferredType())) | ||
88 | ); | ||
89 | } | ||
90 | |||
91 | @Test | ||
92 | void consistentMayNotTest() { | ||
93 | var a1Result = tester.getPreservedType(a1); | ||
94 | var a3Result = tester.getPreservedType(a3); | ||
95 | var a4Result = tester.getPreservedType(a4); | ||
96 | assertAll( | ||
97 | () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE), | ||
98 | is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), | ||
99 | () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | ||
100 | is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), | ||
101 | () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE), | ||
102 | is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), | ||
103 | () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE), | ||
104 | is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))), | ||
105 | () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE), | ||
106 | is(new InferredType(Set.of(), Set.of(c3, c4), null))), | ||
107 | () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE), | ||
108 | is(new InferredType(Set.of(), Set.of(c1, c4), null))), | ||
109 | () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE), | ||
110 | is(new InferredType(Set.of(), Set.of(c3), null))) | ||
111 | ); | ||
112 | } | ||
113 | |||
114 | @Test | ||
115 | void consistentErrorTest() { | ||
116 | var c1Result = tester.getPreservedType(c1); | ||
117 | var a4Result = tester.getPreservedType(a4); | ||
118 | var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null); | ||
119 | assertAll( | ||
120 | () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), is(expected)), | ||
121 | () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), is(expected)) | ||
122 | ); | ||
123 | } | ||
124 | |||
125 | @Test | ||
126 | void consistentUnknownTest() { | ||
127 | var c1Result = tester.getPreservedType(c1); | ||
128 | var a4Result = tester.getPreservedType(a4); | ||
129 | assertAll( | ||
130 | () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.UNKNOWN), | ||
131 | is(a4Result.asInferredType())), | ||
132 | () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.UNKNOWN), | ||
133 | is(c1Result.asInferredType())) | ||
134 | ); | ||
135 | } | ||
136 | |||
137 | @Test | ||
138 | void inconsistentMustTest() { | ||
139 | var a1Result = tester.getPreservedType(a1); | ||
140 | var c3Result = tester.getPreservedType(c3); | ||
141 | assertAll( | ||
142 | () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE), | ||
143 | is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))), | ||
144 | () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), | ||
145 | is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null))) | ||
146 | ); | ||
147 | } | ||
148 | |||
149 | @Test | ||
150 | void inconsistentMayNotTest() { | ||
151 | var a1Result = tester.getPreservedType(a1); | ||
152 | var a4Result = tester.getPreservedType(a4); | ||
153 | var c1Result = tester.getPreservedType(c1); | ||
154 | assertAll( | ||
155 | () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | ||
156 | is(new InferredType(Set.of(a1, a4), Set.of(), null))), | ||
157 | () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE), | ||
158 | is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), | ||
159 | () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE), | ||
160 | is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), | ||
161 | () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | ||
162 | is(new InferredType(Set.of(a1, a4), Set.of(), null))) | ||
163 | ); | ||
164 | } | ||
165 | |||
166 | @Test | ||
167 | void vacuousMustTest() { | ||
168 | var c1Result = tester.getPreservedType(c1); | ||
169 | var a5Result = tester.getPreservedType(a5); | ||
170 | assertAll( | ||
171 | () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE), | ||
172 | is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), | ||
173 | () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE), | ||
174 | is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))) | ||
175 | ); | ||
176 | } | ||
177 | |||
178 | @Test | ||
179 | void vacuousMayNotTest() { | ||
180 | var c1Result = tester.getPreservedType(c1); | ||
181 | var a5Result = tester.getPreservedType(a5); | ||
182 | assertAll( | ||
183 | () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.FALSE), | ||
184 | is(a5Result.asInferredType())), | ||
185 | () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.FALSE), | ||
186 | is(c1Result.asInferredType())) | ||
187 | ); | ||
188 | } | ||
189 | |||
190 | @Test | ||
191 | void vacuousErrorTest() { | ||
192 | var c1Result = tester.getPreservedType(c1); | ||
193 | var a5Result = tester.getPreservedType(a5); | ||
194 | assertAll( | ||
195 | () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR), | ||
196 | is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), | ||
197 | () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR), | ||
198 | is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), | ||
199 | () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR), | ||
200 | is(a5Result.asInferredType())) | ||
201 | ); | ||
202 | } | ||
203 | } | ||
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 new file mode 100644 index 00000000..b7b69ed8 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java | |||
@@ -0,0 +1,200 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import org.junit.jupiter.api.Test; | ||
4 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
5 | import tools.refinery.store.representation.TruthValue; | ||
6 | |||
7 | import java.util.LinkedHashMap; | ||
8 | import java.util.Set; | ||
9 | |||
10 | import static org.hamcrest.MatcherAssert.assertThat; | ||
11 | import static org.hamcrest.Matchers.is; | ||
12 | import static org.junit.jupiter.api.Assertions.assertAll; | ||
13 | import static org.junit.jupiter.api.Assertions.assertThrows; | ||
14 | |||
15 | class TypeAnalyzerTest { | ||
16 | @Test | ||
17 | void directSupertypesTest() { | ||
18 | var c1 = new PartialRelation("C1", 1); | ||
19 | var c2 = new PartialRelation("C2", 1); | ||
20 | var c3 = new PartialRelation("C3", 1); | ||
21 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | ||
22 | typeInfoMap.put(c1, TypeInfo.builder().supertypes(c2, c3).build()); | ||
23 | typeInfoMap.put(c2, TypeInfo.builder().supertype(c3).build()); | ||
24 | typeInfoMap.put(c3, TypeInfo.builder().build()); | ||
25 | |||
26 | var sut = new TypeAnalyzer(typeInfoMap); | ||
27 | var tester = new TypeAnalyzerTester(sut); | ||
28 | |||
29 | assertAll( | ||
30 | () -> tester.assertConcreteType(c1), | ||
31 | () -> tester.assertConcreteType(c2, c1), | ||
32 | () -> tester.assertConcreteType(c3, c2) | ||
33 | ); | ||
34 | } | ||
35 | |||
36 | @Test | ||
37 | void typeEliminationAbstractToConcreteTest() { | ||
38 | var c1 = new PartialRelation("C1", 1); | ||
39 | var c2 = new PartialRelation("C2", 1); | ||
40 | var a11 = new PartialRelation("A11", 1); | ||
41 | var a12 = new PartialRelation("A12", 1); | ||
42 | var a21 = new PartialRelation("A21", 1); | ||
43 | var a22 = new PartialRelation("A22", 1); | ||
44 | var a3 = new PartialRelation("A3", 1); | ||
45 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | ||
46 | typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); | ||
47 | typeInfoMap.put(a21, TypeInfo.builder().abstractType().supertype(a3).build()); | ||
48 | typeInfoMap.put(a22, TypeInfo.builder().abstractType().supertype(a3).build()); | ||
49 | typeInfoMap.put(a11, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); | ||
50 | typeInfoMap.put(a12, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); | ||
51 | typeInfoMap.put(c1, TypeInfo.builder().supertypes(a11, a12).build()); | ||
52 | typeInfoMap.put(c2, TypeInfo.builder().supertype(a3).build()); | ||
53 | |||
54 | var sut = new TypeAnalyzer(typeInfoMap); | ||
55 | var tester = new TypeAnalyzerTester(sut); | ||
56 | |||
57 | assertAll( | ||
58 | () -> tester.assertConcreteType(c1), | ||
59 | () -> tester.assertConcreteType(c2), | ||
60 | () -> tester.assertEliminatedType(a11, c1), | ||
61 | () -> tester.assertEliminatedType(a12, c1), | ||
62 | () -> tester.assertEliminatedType(a21, c1), | ||
63 | () -> tester.assertEliminatedType(a22, c1), | ||
64 | () -> tester.assertAbstractType(a3, c1, c2) | ||
65 | ); | ||
66 | } | ||
67 | |||
68 | @Test | ||
69 | void typeEliminationConcreteToAbstractTest() { | ||
70 | var c1 = new PartialRelation("C1", 1); | ||
71 | var c2 = new PartialRelation("C2", 1); | ||
72 | var a11 = new PartialRelation("A11", 1); | ||
73 | var a12 = new PartialRelation("A12", 1); | ||
74 | var a21 = new PartialRelation("A21", 1); | ||
75 | var a22 = new PartialRelation("A22", 1); | ||
76 | var a3 = new PartialRelation("A3", 1); | ||
77 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | ||
78 | typeInfoMap.put(c1, TypeInfo.builder().supertypes(a11, a12).build()); | ||
79 | typeInfoMap.put(c2, TypeInfo.builder().supertype(a3).build()); | ||
80 | typeInfoMap.put(a11, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); | ||
81 | typeInfoMap.put(a12, TypeInfo.builder().abstractType().supertypes(a21, a22).build()); | ||
82 | typeInfoMap.put(a21, TypeInfo.builder().abstractType().supertype(a3).build()); | ||
83 | typeInfoMap.put(a22, TypeInfo.builder().abstractType().supertype(a3).build()); | ||
84 | typeInfoMap.put(a3, TypeInfo.builder().abstractType().build()); | ||
85 | |||
86 | var sut = new TypeAnalyzer(typeInfoMap); | ||
87 | var tester = new TypeAnalyzerTester(sut); | ||
88 | |||
89 | assertAll( | ||
90 | () -> tester.assertConcreteType(c1), | ||
91 | () -> tester.assertConcreteType(c2), | ||
92 | () -> tester.assertEliminatedType(a11, c1), | ||
93 | () -> tester.assertEliminatedType(a12, c1), | ||
94 | () -> tester.assertEliminatedType(a21, c1), | ||
95 | () -> tester.assertEliminatedType(a22, c1), | ||
96 | () -> tester.assertAbstractType(a3, c1, c2) | ||
97 | ); | ||
98 | } | ||
99 | |||
100 | @Test | ||
101 | void preserveConcreteTypeTest() { | ||
102 | var c1 = new PartialRelation("C1", 1); | ||
103 | var a1 = new PartialRelation("A1", 1); | ||
104 | var c2 = new PartialRelation("C2", 1); | ||
105 | var a2 = new PartialRelation("A2", 1); | ||
106 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | ||
107 | typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); | ||
108 | typeInfoMap.put(a1, TypeInfo.builder().abstractType().supertype(c2).build()); | ||
109 | typeInfoMap.put(c2, TypeInfo.builder().supertype(a2).build()); | ||
110 | typeInfoMap.put(a2, TypeInfo.builder().abstractType().build()); | ||
111 | |||
112 | var sut = new TypeAnalyzer(typeInfoMap); | ||
113 | var tester = new TypeAnalyzerTester(sut); | ||
114 | |||
115 | assertAll( | ||
116 | () -> tester.assertConcreteType(c1), | ||
117 | () -> tester.assertEliminatedType(a1, c1), | ||
118 | () -> tester.assertConcreteType(c2, c1), | ||
119 | () -> tester.assertEliminatedType(a2, c2) | ||
120 | ); | ||
121 | } | ||
122 | |||
123 | @Test | ||
124 | void mostGeneralCurrentTypeTest() { | ||
125 | var c1 = new PartialRelation("C1", 1); | ||
126 | var c2 = new PartialRelation("C2", 1); | ||
127 | var c3 = new PartialRelation("C3", 1); | ||
128 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | ||
129 | typeInfoMap.put(c1, TypeInfo.builder().supertype(c3).build()); | ||
130 | typeInfoMap.put(c2, TypeInfo.builder().supertype(c3).build()); | ||
131 | typeInfoMap.put(c3, TypeInfo.builder().build()); | ||
132 | |||
133 | var sut = new TypeAnalyzer(typeInfoMap); | ||
134 | var tester = new TypeAnalyzerTester(sut); | ||
135 | var c3Result = tester.getPreservedType(c3); | ||
136 | |||
137 | var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3); | ||
138 | assertAll( | ||
139 | () -> assertThat(tester.getInferredType(c3), is(expected)), | ||
140 | () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(expected)) | ||
141 | ); | ||
142 | } | ||
143 | |||
144 | @Test | ||
145 | void preferFirstConcreteTypeTest() { | ||
146 | var a1 = new PartialRelation("A1", 1); | ||
147 | var c1 = new PartialRelation("C1", 1); | ||
148 | var c2 = new PartialRelation("C2", 1); | ||
149 | var c3 = new PartialRelation("C3", 1); | ||
150 | var c4 = new PartialRelation("C4", 1); | ||
151 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | ||
152 | typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); | ||
153 | typeInfoMap.put(c2, TypeInfo.builder().supertype(a1).build()); | ||
154 | typeInfoMap.put(c3, TypeInfo.builder().supertype(a1).build()); | ||
155 | typeInfoMap.put(c4, TypeInfo.builder().supertype(c3).build()); | ||
156 | typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); | ||
157 | |||
158 | var sut = new TypeAnalyzer(typeInfoMap); | ||
159 | var tester = new TypeAnalyzerTester(sut); | ||
160 | var c1Result = tester.getPreservedType(c1); | ||
161 | var a1Result = tester.getPreservedType(a1); | ||
162 | |||
163 | assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | ||
164 | is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2))); | ||
165 | } | ||
166 | |||
167 | @Test | ||
168 | void preferFirstMostGeneralConcreteTypeTest() { | ||
169 | var a1 = new PartialRelation("A1", 1); | ||
170 | var c1 = new PartialRelation("C1", 1); | ||
171 | var c2 = new PartialRelation("C2", 1); | ||
172 | var c3 = new PartialRelation("C3", 1); | ||
173 | var c4 = new PartialRelation("C4", 1); | ||
174 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | ||
175 | typeInfoMap.put(c4, TypeInfo.builder().supertype(c3).build()); | ||
176 | typeInfoMap.put(c3, TypeInfo.builder().supertype(a1).build()); | ||
177 | typeInfoMap.put(c2, TypeInfo.builder().supertype(a1).build()); | ||
178 | typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build()); | ||
179 | typeInfoMap.put(a1, TypeInfo.builder().abstractType().build()); | ||
180 | |||
181 | var sut = new TypeAnalyzer(typeInfoMap); | ||
182 | var tester = new TypeAnalyzerTester(sut); | ||
183 | var c1Result = tester.getPreservedType(c1); | ||
184 | var a1Result = tester.getPreservedType(a1); | ||
185 | |||
186 | assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | ||
187 | is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3))); | ||
188 | } | ||
189 | |||
190 | @Test | ||
191 | void circularTypeHierarchyTest() { | ||
192 | var c1 = new PartialRelation("C1", 1); | ||
193 | var c2 = new PartialRelation("C2", 1); | ||
194 | var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>(); | ||
195 | typeInfoMap.put(c1, TypeInfo.builder().supertype(c2).build()); | ||
196 | typeInfoMap.put(c2, TypeInfo.builder().supertype(c1).build()); | ||
197 | |||
198 | assertThrows(IllegalArgumentException.class, () -> new TypeAnalyzer(typeInfoMap)); | ||
199 | } | ||
200 | } | ||
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTester.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTester.java new file mode 100644 index 00000000..56407730 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTester.java | |||
@@ -0,0 +1,51 @@ | |||
1 | package tools.refinery.store.reasoning.translator.typehierarchy; | ||
2 | |||
3 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
4 | |||
5 | import static org.hamcrest.MatcherAssert.assertThat; | ||
6 | import static org.hamcrest.Matchers.*; | ||
7 | import static org.hamcrest.Matchers.is; | ||
8 | |||
9 | class TypeAnalyzerTester { | ||
10 | private final TypeAnalyzer sut; | ||
11 | |||
12 | public TypeAnalyzerTester(TypeAnalyzer sut) { | ||
13 | this.sut = sut; | ||
14 | } | ||
15 | |||
16 | public void assertAbstractType(PartialRelation partialRelation, PartialRelation... directSubtypes) { | ||
17 | assertPreservedType(partialRelation, true, false, directSubtypes); | ||
18 | } | ||
19 | |||
20 | public void assertVacuousType(PartialRelation partialRelation) { | ||
21 | assertPreservedType(partialRelation, true, true); | ||
22 | } | ||
23 | |||
24 | public void assertConcreteType(PartialRelation partialRelation, PartialRelation... directSubtypes) { | ||
25 | assertPreservedType(partialRelation, false, false, directSubtypes); | ||
26 | } | ||
27 | |||
28 | private void assertPreservedType(PartialRelation partialRelation, boolean isAbstract, boolean isVacuous, | ||
29 | PartialRelation... directSubtypes) { | ||
30 | var result = sut.getAnalysisResults().get(partialRelation); | ||
31 | assertThat(result, is(instanceOf(PreservedType.class))); | ||
32 | var preservedResult = (PreservedType) result; | ||
33 | assertThat(preservedResult.isAbstractType(), is(isAbstract)); | ||
34 | assertThat(preservedResult.isVacuous(), is(isVacuous)); | ||
35 | assertThat(preservedResult.getDirectSubtypes(), hasItems(directSubtypes)); | ||
36 | } | ||
37 | |||
38 | public void assertEliminatedType(PartialRelation partialRelation, PartialRelation replacement) { | ||
39 | var result = sut.getAnalysisResults().get(partialRelation); | ||
40 | assertThat(result, is(instanceOf(EliminatedType.class))); | ||
41 | assertThat(((EliminatedType) result).replacement(), is(replacement)); | ||
42 | } | ||
43 | |||
44 | public PreservedType getPreservedType(PartialRelation partialRelation) { | ||
45 | return (PreservedType) sut.getAnalysisResults().get(partialRelation); | ||
46 | } | ||
47 | |||
48 | public InferredType getInferredType(PartialRelation partialRelation) { | ||
49 | return getPreservedType(partialRelation).asInferredType(); | ||
50 | } | ||
51 | } | ||