diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-02-20 20:23:27 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-02-20 20:23:27 +0100 |
commit | b3f7c4d7707435803921c4fec2c4d95b3dd45c53 (patch) | |
tree | 18a90112efe3ece8678709db322dddcefafaace1 /subprojects | |
parent | feat: type inference for class hierarchies (diff) | |
download | refinery-b3f7c4d7707435803921c4fec2c4d95b3dd45c53.tar.gz refinery-b3f7c4d7707435803921c4fec2c4d95b3dd45c53.tar.zst refinery-b3f7c4d7707435803921c4fec2c4d95b3dd45c53.zip |
refactor: split query and partial from store
Allows more complicated dependency hiearchies (e.g., use
store-query-viatra for testing store-partial) and better separation of
test fixtures.
Diffstat (limited to 'subprojects')
82 files changed, 1093 insertions, 246 deletions
diff --git a/subprojects/store-partial/build.gradle b/subprojects/store-partial/build.gradle new file mode 100644 index 00000000..cb440d9f --- /dev/null +++ b/subprojects/store-partial/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-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java new file mode 100644 index 00000000..b6b1f2be --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java | |||
@@ -0,0 +1,13 @@ | |||
1 | package tools.refinery.store.partial; | ||
2 | |||
3 | import tools.refinery.store.partial.representation.AnyPartialSymbol; | ||
4 | |||
5 | public sealed interface AnyPartialSymbolInterpretation permits PartialSymbolInterpretation { | ||
6 | PartialInterpretationAdapter getAdapter(); | ||
7 | |||
8 | AnyPartialSymbol getPartialSymbol(); | ||
9 | |||
10 | int countUnfinished(); | ||
11 | |||
12 | int countErrors(); | ||
13 | } | ||
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java new file mode 100644 index 00000000..82414d87 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java | |||
@@ -0,0 +1,15 @@ | |||
1 | package tools.refinery.store.partial; | ||
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/src/main/java/tools/refinery/store/partial/PartialInterpretation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretation.java index 331fa294..d76f8728 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretation.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretation.java | |||
@@ -1,13 +1,18 @@ | |||
1 | package tools.refinery.store.partial; | 1 | package tools.refinery.store.partial; |
2 | 2 | ||
3 | import tools.refinery.store.partial.internal.PartialInterpretationBuilderImpl; | ||
3 | import tools.refinery.store.adapter.ModelAdapterBuilderFactory; | 4 | import tools.refinery.store.adapter.ModelAdapterBuilderFactory; |
4 | import tools.refinery.store.model.ModelStoreBuilder; | 5 | import tools.refinery.store.model.ModelStoreBuilder; |
5 | import tools.refinery.store.partial.internal.PartialInterpretationBuilderImpl; | 6 | import tools.refinery.store.partial.representation.PartialRelation; |
6 | 7 | ||
7 | public final class PartialInterpretation extends ModelAdapterBuilderFactory<PartialInterpretationAdapter, | 8 | public final class PartialInterpretation extends ModelAdapterBuilderFactory<PartialInterpretationAdapter, |
8 | PartialInterpretationStoreAdapter, PartialInterpretationBuilder> { | 9 | PartialInterpretationStoreAdapter, PartialInterpretationBuilder> { |
9 | public static final PartialInterpretation ADAPTER = new PartialInterpretation(); | 10 | public static final PartialInterpretation ADAPTER = new PartialInterpretation(); |
10 | 11 | ||
12 | public static final PartialRelation EXISTS = new PartialRelation("exists", 1); | ||
13 | |||
14 | public static final PartialRelation EQUALS = new PartialRelation("equals", 1); | ||
15 | |||
11 | private PartialInterpretation() { | 16 | private PartialInterpretation() { |
12 | super(PartialInterpretationAdapter.class, PartialInterpretationStoreAdapter.class, PartialInterpretationBuilder.class); | 17 | super(PartialInterpretationAdapter.class, PartialInterpretationStoreAdapter.class, PartialInterpretationBuilder.class); |
13 | } | 18 | } |
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java new file mode 100644 index 00000000..b811ae7a --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java | |||
@@ -0,0 +1,20 @@ | |||
1 | package tools.refinery.store.partial; | ||
2 | |||
3 | import tools.refinery.store.adapter.ModelAdapter; | ||
4 | import tools.refinery.store.partial.representation.AnyPartialSymbol; | ||
5 | import tools.refinery.store.partial.representation.PartialSymbol; | ||
6 | import tools.refinery.store.query.Dnf; | ||
7 | import tools.refinery.store.query.ResultSet; | ||
8 | |||
9 | public interface PartialInterpretationAdapter extends ModelAdapter { | ||
10 | @Override | ||
11 | PartialInterpretationStoreAdapter getStoreAdapter(); | ||
12 | |||
13 | default AnyPartialSymbolInterpretation getPartialInterpretation(AnyPartialSymbol partialSymbol) { | ||
14 | return getPartialInterpretation((PartialSymbol<?, ?>) partialSymbol); | ||
15 | } | ||
16 | |||
17 | <A, C> PartialSymbolInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol); | ||
18 | |||
19 | ResultSet getLiftedResultSet(Dnf query); | ||
20 | } | ||
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java new file mode 100644 index 00000000..db042466 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java | |||
@@ -0,0 +1,28 @@ | |||
1 | package tools.refinery.store.partial; | ||
2 | |||
3 | import tools.refinery.store.adapter.ModelAdapterBuilder; | ||
4 | import tools.refinery.store.model.ModelStore; | ||
5 | import tools.refinery.store.query.Dnf; | ||
6 | import tools.refinery.store.partial.literal.Modality; | ||
7 | |||
8 | import java.util.Collection; | ||
9 | import java.util.List; | ||
10 | |||
11 | @SuppressWarnings("UnusedReturnValue") | ||
12 | public interface PartialInterpretationBuilder extends ModelAdapterBuilder { | ||
13 | default PartialInterpretationBuilder liftedQueries(Dnf... liftedQueries) { | ||
14 | return liftedQueries(List.of(liftedQueries)); | ||
15 | } | ||
16 | |||
17 | default PartialInterpretationBuilder liftedQueries(Collection<Dnf> liftedQueries) { | ||
18 | liftedQueries.forEach(this::liftedQuery); | ||
19 | return this; | ||
20 | } | ||
21 | |||
22 | PartialInterpretationBuilder liftedQuery(Dnf liftedQuery); | ||
23 | |||
24 | Dnf lift(Modality modality, Dnf query); | ||
25 | |||
26 | @Override | ||
27 | PartialInterpretationStoreAdapter createStoreAdapter(ModelStore store); | ||
28 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java index d4eb770d..a1813671 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java | |||
@@ -2,8 +2,16 @@ package tools.refinery.store.partial; | |||
2 | 2 | ||
3 | import tools.refinery.store.adapter.ModelStoreAdapter; | 3 | import tools.refinery.store.adapter.ModelStoreAdapter; |
4 | import tools.refinery.store.model.Model; | 4 | import tools.refinery.store.model.Model; |
5 | import tools.refinery.store.partial.representation.AnyPartialSymbol; | ||
6 | import tools.refinery.store.query.Dnf; | ||
7 | |||
8 | import java.util.Collection; | ||
5 | 9 | ||
6 | public interface PartialInterpretationStoreAdapter extends ModelStoreAdapter { | 10 | public interface PartialInterpretationStoreAdapter extends ModelStoreAdapter { |
11 | Collection<AnyPartialSymbol> getPartialSymbols(); | ||
12 | |||
13 | Collection<Dnf> getLiftedQueries(); | ||
14 | |||
7 | @Override | 15 | @Override |
8 | PartialInterpretationAdapter createModelAdapter(Model model); | 16 | PartialInterpretationAdapter createModelAdapter(Model model); |
9 | } | 17 | } |
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java new file mode 100644 index 00000000..fa9e9216 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java | |||
@@ -0,0 +1,22 @@ | |||
1 | package tools.refinery.store.partial; | ||
2 | |||
3 | import tools.refinery.store.partial.representation.PartialSymbol; | ||
4 | import tools.refinery.store.map.Cursor; | ||
5 | import tools.refinery.store.tuple.Tuple; | ||
6 | |||
7 | public non-sealed interface PartialSymbolInterpretation<A, C> extends AnyPartialSymbolInterpretation { | ||
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/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java index 4b3977c0..c482d8a2 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java | |||
@@ -2,6 +2,10 @@ package tools.refinery.store.partial.internal; | |||
2 | 2 | ||
3 | import tools.refinery.store.model.Model; | 3 | import tools.refinery.store.model.Model; |
4 | import tools.refinery.store.partial.PartialInterpretationAdapter; | 4 | import tools.refinery.store.partial.PartialInterpretationAdapter; |
5 | import tools.refinery.store.partial.PartialSymbolInterpretation; | ||
6 | import tools.refinery.store.partial.representation.PartialSymbol; | ||
7 | import tools.refinery.store.query.Dnf; | ||
8 | import tools.refinery.store.query.ResultSet; | ||
5 | 9 | ||
6 | public class PartialInterpretationAdapterImpl implements PartialInterpretationAdapter { | 10 | public class PartialInterpretationAdapterImpl implements PartialInterpretationAdapter { |
7 | private final Model model; | 11 | private final Model model; |
@@ -21,4 +25,14 @@ public class PartialInterpretationAdapterImpl implements PartialInterpretationAd | |||
21 | public PartialInterpretationStoreAdapterImpl getStoreAdapter() { | 25 | public PartialInterpretationStoreAdapterImpl getStoreAdapter() { |
22 | return storeAdapter; | 26 | return storeAdapter; |
23 | } | 27 | } |
28 | |||
29 | @Override | ||
30 | public <A, C> PartialSymbolInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) { | ||
31 | return null; | ||
32 | } | ||
33 | |||
34 | @Override | ||
35 | public ResultSet getLiftedResultSet(Dnf query) { | ||
36 | return null; | ||
37 | } | ||
24 | } | 38 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java index 4609dc32..5853aeaf 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java | |||
@@ -4,6 +4,8 @@ import tools.refinery.store.adapter.AbstractModelAdapterBuilder; | |||
4 | import tools.refinery.store.model.ModelStore; | 4 | import tools.refinery.store.model.ModelStore; |
5 | import tools.refinery.store.model.ModelStoreBuilder; | 5 | import tools.refinery.store.model.ModelStoreBuilder; |
6 | import tools.refinery.store.partial.PartialInterpretationBuilder; | 6 | import tools.refinery.store.partial.PartialInterpretationBuilder; |
7 | import tools.refinery.store.partial.literal.Modality; | ||
8 | import tools.refinery.store.query.Dnf; | ||
7 | 9 | ||
8 | public class PartialInterpretationBuilderImpl extends AbstractModelAdapterBuilder implements PartialInterpretationBuilder { | 10 | public class PartialInterpretationBuilderImpl extends AbstractModelAdapterBuilder implements PartialInterpretationBuilder { |
9 | public PartialInterpretationBuilderImpl(ModelStoreBuilder storeBuilder) { | 11 | public PartialInterpretationBuilderImpl(ModelStoreBuilder storeBuilder) { |
@@ -11,6 +13,16 @@ public class PartialInterpretationBuilderImpl extends AbstractModelAdapterBuilde | |||
11 | } | 13 | } |
12 | 14 | ||
13 | @Override | 15 | @Override |
16 | public PartialInterpretationBuilder 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 | ||
14 | public PartialInterpretationStoreAdapterImpl createStoreAdapter(ModelStore store) { | 26 | public PartialInterpretationStoreAdapterImpl createStoreAdapter(ModelStore store) { |
15 | return null; | 27 | return null; |
16 | } | 28 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java index 970b802b..0486af6e 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java | |||
@@ -1,8 +1,12 @@ | |||
1 | package tools.refinery.store.partial.internal; | 1 | package tools.refinery.store.partial.internal; |
2 | 2 | ||
3 | import tools.refinery.store.partial.PartialInterpretationStoreAdapter; | ||
3 | import tools.refinery.store.model.Model; | 4 | import tools.refinery.store.model.Model; |
4 | import tools.refinery.store.model.ModelStore; | 5 | import tools.refinery.store.model.ModelStore; |
5 | import tools.refinery.store.partial.PartialInterpretationStoreAdapter; | 6 | import tools.refinery.store.partial.representation.AnyPartialSymbol; |
7 | import tools.refinery.store.query.Dnf; | ||
8 | |||
9 | import java.util.Collection; | ||
6 | 10 | ||
7 | public class PartialInterpretationStoreAdapterImpl implements PartialInterpretationStoreAdapter { | 11 | public class PartialInterpretationStoreAdapterImpl implements PartialInterpretationStoreAdapter { |
8 | private final ModelStore store; | 12 | private final ModelStore store; |
@@ -17,6 +21,16 @@ public class PartialInterpretationStoreAdapterImpl implements PartialInterpretat | |||
17 | } | 21 | } |
18 | 22 | ||
19 | @Override | 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 | ||
20 | public PartialInterpretationAdapterImpl createModelAdapter(Model model) { | 34 | public PartialInterpretationAdapterImpl createModelAdapter(Model model) { |
21 | return new PartialInterpretationAdapterImpl(model, this); | 35 | return new PartialInterpretationAdapterImpl(model, this); |
22 | } | 36 | } |
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java new file mode 100644 index 00000000..1c35b925 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java | |||
@@ -0,0 +1,107 @@ | |||
1 | package tools.refinery.store.partial.lifting; | ||
2 | |||
3 | import org.jetbrains.annotations.Nullable; | ||
4 | import tools.refinery.store.partial.literal.ModalDnfCallLiteral; | ||
5 | import tools.refinery.store.partial.PartialInterpretation; | ||
6 | import tools.refinery.store.partial.literal.ModalRelationLiteral; | ||
7 | import tools.refinery.store.partial.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.partial.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(PartialInterpretation.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(PartialInterpretation.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-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java new file mode 100644 index 00000000..6fe54ad9 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java | |||
@@ -0,0 +1,11 @@ | |||
1 | package tools.refinery.store.partial.lifting; | ||
2 | |||
3 | import tools.refinery.store.query.Dnf; | ||
4 | import tools.refinery.store.partial.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/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java index 8070726a..a49e0625 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java | |||
@@ -4,6 +4,7 @@ import tools.refinery.store.query.Dnf; | |||
4 | import tools.refinery.store.query.Variable; | 4 | import tools.refinery.store.query.Variable; |
5 | import tools.refinery.store.query.literal.CallPolarity; | 5 | import tools.refinery.store.query.literal.CallPolarity; |
6 | import tools.refinery.store.query.literal.DnfCallLiteral; | 6 | import tools.refinery.store.query.literal.DnfCallLiteral; |
7 | import tools.refinery.store.query.literal.LiteralReduction; | ||
7 | import tools.refinery.store.query.literal.PolarLiteral; | 8 | import tools.refinery.store.query.literal.PolarLiteral; |
8 | 9 | ||
9 | import java.util.List; | 10 | import java.util.List; |
@@ -27,4 +28,10 @@ public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiter | |||
27 | public ModalDnfCallLiteral negate() { | 28 | public ModalDnfCallLiteral negate() { |
28 | return new ModalDnfCallLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); | 29 | return new ModalDnfCallLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); |
29 | } | 30 | } |
31 | |||
32 | @Override | ||
33 | public LiteralReduction getReduction() { | ||
34 | var dnfReduction = getTarget().getReduction(); | ||
35 | return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate(); | ||
36 | } | ||
30 | } | 37 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java index a1b6c83e..a1b6c83e 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java index dbaa524f..dbaa524f 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/Modality.java index d647ef0a..d647ef0a 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/Modality.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java index 51d388d3..51d388d3 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java index dc1a1da3..dc1a1da3 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java index 1113245e..1113245e 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java index 25096e74..25096e74 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java index 3c186f6f..3c186f6f 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java index 127355ca..51c2f28d 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java | |||
@@ -1,11 +1,11 @@ | |||
1 | package tools.refinery.store.partial.representation; | 1 | package tools.refinery.store.partial.representation; |
2 | 2 | ||
3 | import tools.refinery.store.partial.literal.ModalRelationLiteral; | 3 | import tools.refinery.store.partial.literal.Modality; |
4 | import tools.refinery.store.partial.literal.PartialRelationLiteral; | 4 | import tools.refinery.store.partial.literal.PartialRelationLiteral; |
5 | import tools.refinery.store.partial.literal.ModalRelationLiteral; | ||
5 | import tools.refinery.store.query.RelationLike; | 6 | import tools.refinery.store.query.RelationLike; |
6 | import tools.refinery.store.query.Variable; | 7 | import tools.refinery.store.query.Variable; |
7 | import tools.refinery.store.query.literal.CallPolarity; | 8 | import tools.refinery.store.query.literal.CallPolarity; |
8 | import tools.refinery.store.partial.literal.Modality; | ||
9 | import tools.refinery.store.representation.AbstractDomain; | 9 | import tools.refinery.store.representation.AbstractDomain; |
10 | import tools.refinery.store.representation.TruthValue; | 10 | import tools.refinery.store.representation.TruthValue; |
11 | import tools.refinery.store.representation.TruthValueDomain; | 11 | import tools.refinery.store.representation.TruthValueDomain; |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java index 38533fa9..38533fa9 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java | |||
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java new file mode 100644 index 00000000..6c89653d --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java | |||
@@ -0,0 +1,36 @@ | |||
1 | package tools.refinery.store.partial.rule; | ||
2 | |||
3 | import tools.refinery.store.partial.PartialInterpretation; | ||
4 | import tools.refinery.store.partial.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(PartialInterpretation.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-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java new file mode 100644 index 00000000..c114b8cf --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java | |||
@@ -0,0 +1,38 @@ | |||
1 | package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java new file mode 100644 index 00000000..7a8ede40 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java | |||
@@ -0,0 +1,12 @@ | |||
1 | package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java new file mode 100644 index 00000000..1c2db5f1 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java | |||
@@ -0,0 +1,9 @@ | |||
1 | package tools.refinery.store.partial.rule; | ||
2 | |||
3 | import tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java new file mode 100644 index 00000000..41d79306 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java | |||
@@ -0,0 +1,34 @@ | |||
1 | package tools.refinery.store.partial.rule; | ||
2 | |||
3 | import tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java new file mode 100644 index 00000000..65040a8e --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java | |||
@@ -0,0 +1,155 @@ | |||
1 | package tools.refinery.store.partial.translator; | ||
2 | |||
3 | import tools.refinery.store.partial.representation.AnyPartialSymbol; | ||
4 | import tools.refinery.store.partial.representation.PartialRelation; | ||
5 | import tools.refinery.store.query.Variable; | ||
6 | import tools.refinery.store.query.literal.Literal; | ||
7 | |||
8 | import java.util.*; | ||
9 | |||
10 | public final class Advice { | ||
11 | private final AnyPartialSymbol source; | ||
12 | private final PartialRelation target; | ||
13 | private final AdviceSlot slot; | ||
14 | private final boolean mandatory; | ||
15 | private final List<Variable> parameters; | ||
16 | private final List<Literal> literals; | ||
17 | private boolean processed; | ||
18 | |||
19 | public Advice(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot, boolean mandatory, List<Variable> parameters, List<Literal> literals) { | ||
20 | if (mandatory && !slot.isMonotonic()) { | ||
21 | throw new IllegalArgumentException("Only monotonic advice can be mandatory"); | ||
22 | } | ||
23 | this.source = source; | ||
24 | this.target = target; | ||
25 | this.slot = slot; | ||
26 | this.mandatory = mandatory; | ||
27 | checkArity(parameters); | ||
28 | this.parameters = parameters; | ||
29 | this.literals = literals; | ||
30 | } | ||
31 | |||
32 | public AnyPartialSymbol source() { | ||
33 | return source; | ||
34 | } | ||
35 | |||
36 | public PartialRelation target() { | ||
37 | return target; | ||
38 | } | ||
39 | |||
40 | public AdviceSlot slot() { | ||
41 | return slot; | ||
42 | } | ||
43 | |||
44 | public boolean mandatory() { | ||
45 | return mandatory; | ||
46 | } | ||
47 | |||
48 | public List<Variable> parameters() { | ||
49 | return parameters; | ||
50 | } | ||
51 | |||
52 | public List<Literal> literals() { | ||
53 | return literals; | ||
54 | } | ||
55 | |||
56 | public boolean processed() { | ||
57 | return processed; | ||
58 | } | ||
59 | |||
60 | public List<Literal> substitute(List<Variable> substituteParameters) { | ||
61 | checkArity(substituteParameters); | ||
62 | markProcessed(); | ||
63 | int arity = parameters.size(); | ||
64 | var substitution = new HashMap<Variable, Variable>(arity); | ||
65 | for (int i = 0; i < arity; i++) { | ||
66 | substitution.put(parameters.get(i), substituteParameters.get(i)); | ||
67 | } | ||
68 | return literals.stream().map(literal -> literal.substitute(substitution)).toList(); | ||
69 | } | ||
70 | |||
71 | private void markProcessed() { | ||
72 | processed = true; | ||
73 | } | ||
74 | |||
75 | public void checkProcessed() { | ||
76 | if (mandatory && !processed) { | ||
77 | throw new IllegalStateException("Mandatory advice %s was not processed".formatted(this)); | ||
78 | } | ||
79 | } | ||
80 | |||
81 | private void checkArity(List<Variable> toCheck) { | ||
82 | if (toCheck.size() != target.arity()) { | ||
83 | throw new IllegalArgumentException("%s needs %d parameters, but got %s".formatted(target.name(), | ||
84 | target.arity(), parameters.size())); | ||
85 | } | ||
86 | } | ||
87 | |||
88 | public static Builder builderFor(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) { | ||
89 | return new Builder(source, target, slot); | ||
90 | } | ||
91 | |||
92 | |||
93 | @Override | ||
94 | public String toString() { | ||
95 | return "Advice[source=%s, target=%s, slot=%s, mandatory=%s, parameters=%s, literals=%s]".formatted(source, | ||
96 | target, slot, mandatory, parameters, literals); | ||
97 | } | ||
98 | |||
99 | public static class Builder { | ||
100 | private final AnyPartialSymbol source; | ||
101 | private final PartialRelation target; | ||
102 | private final AdviceSlot slot; | ||
103 | private boolean mandatory; | ||
104 | private final List<Variable> parameters = new ArrayList<>(); | ||
105 | private final List<Literal> literals = new ArrayList<>(); | ||
106 | |||
107 | private Builder(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) { | ||
108 | this.source = source; | ||
109 | this.target = target; | ||
110 | this.slot = slot; | ||
111 | } | ||
112 | |||
113 | public Builder mandatory(boolean mandatory) { | ||
114 | this.mandatory = mandatory; | ||
115 | return this; | ||
116 | } | ||
117 | |||
118 | public Builder mandatory() { | ||
119 | return mandatory(false); | ||
120 | } | ||
121 | |||
122 | public Builder parameters(List<Variable> variables) { | ||
123 | parameters.addAll(variables); | ||
124 | return this; | ||
125 | } | ||
126 | |||
127 | public Builder parameters(Variable... variables) { | ||
128 | return parameters(List.of(variables)); | ||
129 | } | ||
130 | |||
131 | public Builder parameter(Variable variable) { | ||
132 | parameters.add(variable); | ||
133 | return this; | ||
134 | } | ||
135 | |||
136 | public Builder literals(Collection<Literal> literals) { | ||
137 | this.literals.addAll(literals); | ||
138 | return this; | ||
139 | } | ||
140 | |||
141 | public Builder literals(Literal... literals) { | ||
142 | return literals(List.of(literals)); | ||
143 | } | ||
144 | |||
145 | public Builder literal(Literal literal) { | ||
146 | literals.add(literal); | ||
147 | return this; | ||
148 | } | ||
149 | |||
150 | public Advice build() { | ||
151 | return new Advice(source, target, slot, mandatory, Collections.unmodifiableList(parameters), | ||
152 | Collections.unmodifiableList(literals)); | ||
153 | } | ||
154 | } | ||
155 | } | ||
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java new file mode 100644 index 00000000..3702a8ac --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java | |||
@@ -0,0 +1,25 @@ | |||
1 | package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java new file mode 100644 index 00000000..c56b06ed --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java | |||
@@ -0,0 +1,12 @@ | |||
1 | package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java new file mode 100644 index 00000000..26bd909b --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java | |||
@@ -0,0 +1,48 @@ | |||
1 | package tools.refinery.store.partial.translator; | ||
2 | |||
3 | import tools.refinery.store.partial.PartialInterpretationBuilder; | ||
4 | import tools.refinery.store.model.Model; | ||
5 | import tools.refinery.store.model.ModelStoreBuilder; | ||
6 | import tools.refinery.store.partial.AnyPartialSymbolInterpretation; | ||
7 | import tools.refinery.store.partial.literal.Modality; | ||
8 | import tools.refinery.store.partial.representation.AnyPartialSymbol; | ||
9 | import tools.refinery.store.partial.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 PartialInterpretationBuilder partialInterpretationBuilder; | ||
20 | |||
21 | protected PartialInterpretationBuilder getPartialInterpretationBuilder() { | ||
22 | return partialInterpretationBuilder; | ||
23 | } | ||
24 | |||
25 | public void setPartialInterpretationBuilder(PartialInterpretationBuilder partialInterpretationBuilder) { | ||
26 | this.partialInterpretationBuilder = partialInterpretationBuilder; | ||
27 | } | ||
28 | |||
29 | protected ModelStoreBuilder getModelStoreBuilder() { | ||
30 | return partialInterpretationBuilder.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, AnyPartialSymbolInterpretation> createPartialInterpretations(Model model); | ||
46 | |||
47 | public abstract void initializeModel(Model model, int nodeCount); | ||
48 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java index 9adf6bc8..9adf6bc8 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java index d3f66a4c..d3f66a4c 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java | |||
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java new file mode 100644 index 00000000..ff761936 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java | |||
@@ -0,0 +1,19 @@ | |||
1 | package tools.refinery.store.partial.translator.typehierarchy; | ||
2 | |||
3 | import tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java new file mode 100644 index 00000000..4eca0a1c --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java | |||
@@ -0,0 +1,19 @@ | |||
1 | package tools.refinery.store.partial.translator.typehierarchy; | ||
2 | |||
3 | import tools.refinery.store.partial.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/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java index 729b1fb5..729b1fb5 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java index 0299ae03..0299ae03 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java index 0745f84e..0745f84e 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java index 062b4c49..062b4c49 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java | |||
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java new file mode 100644 index 00000000..7f438f71 --- /dev/null +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java | |||
@@ -0,0 +1,52 @@ | |||
1 | package tools.refinery.store.partial.translator.typehierarchy; | ||
2 | |||
3 | import tools.refinery.store.partial.AnyPartialSymbolInterpretation; | ||
4 | import tools.refinery.store.partial.literal.Modality; | ||
5 | import tools.refinery.store.partial.representation.AnyPartialSymbol; | ||
6 | import tools.refinery.store.partial.representation.PartialRelation; | ||
7 | import tools.refinery.store.partial.translator.Advice; | ||
8 | import tools.refinery.store.partial.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 Map<PartialRelation, TypeInfo> typeInfoMap; | ||
22 | |||
23 | public TypeHierarchyTranslationUnit(Map<PartialRelation, TypeInfo> typeInfoMap) { | ||
24 | this.typeInfoMap = new LinkedHashMap<>(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, AnyPartialSymbolInterpretation> 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/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java index 1b0922fe..1b0922fe 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java +++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java | |||
diff --git a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java index 9efa76ef..9efa76ef 100644 --- a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java +++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/InferredTypeTest.java | |||
diff --git a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java index 5f528328..ad81e28f 100644 --- a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java +++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java | |||
@@ -1,5 +1,6 @@ | |||
1 | package tools.refinery.store.partial.translator.typehierarchy; | 1 | package tools.refinery.store.partial.translator.typehierarchy; |
2 | 2 | ||
3 | import org.hamcrest.Matchers; | ||
3 | import org.junit.jupiter.api.BeforeEach; | 4 | import org.junit.jupiter.api.BeforeEach; |
4 | import org.junit.jupiter.api.Test; | 5 | import org.junit.jupiter.api.Test; |
5 | import tools.refinery.store.partial.representation.PartialRelation; | 6 | import tools.refinery.store.partial.representation.PartialRelation; |
@@ -60,16 +61,16 @@ class TypeAnalyzerExampleHierarchyTest { | |||
60 | @Test | 61 | @Test |
61 | void inferredTypesTest() { | 62 | void inferredTypesTest() { |
62 | assertAll( | 63 | assertAll( |
63 | () -> assertThat(sut.getUnknownType(), is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))), | 64 | () -> assertThat(sut.getUnknownType(), Matchers.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(a1), Matchers.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(a3), Matchers.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(a4), Matchers.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(a5), Matchers.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(c1), Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), |
69 | () -> assertThat(tester.getInferredType(c2), | 70 | () -> assertThat(tester.getInferredType(c2), |
70 | is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))), | 71 | Matchers.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(c3), Matchers.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 | () -> assertThat(tester.getInferredType(c4), Matchers.is(new InferredType(Set.of(a4, c4), Set.of(c4), c4))) |
73 | ); | 74 | ); |
74 | } | 75 | } |
75 | 76 | ||
@@ -79,8 +80,8 @@ class TypeAnalyzerExampleHierarchyTest { | |||
79 | var a3Result = tester.getPreservedType(a3); | 80 | var a3Result = tester.getPreservedType(a3); |
80 | var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2); | 81 | var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2); |
81 | assertAll( | 82 | assertAll( |
82 | () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), is(expected)), | 83 | () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)), |
83 | () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), is(expected)), | 84 | () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)), |
84 | () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())), | 85 | () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())), |
85 | () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())), | 86 | () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())), |
86 | () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE), | 87 | () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE), |
@@ -95,19 +96,19 @@ class TypeAnalyzerExampleHierarchyTest { | |||
95 | var a4Result = tester.getPreservedType(a4); | 96 | var a4Result = tester.getPreservedType(a4); |
96 | assertAll( | 97 | assertAll( |
97 | () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE), | 98 | () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE), |
98 | is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), | 99 | Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), |
99 | () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | 100 | () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE), |
100 | is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), | 101 | Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))), |
101 | () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE), | 102 | () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE), |
102 | is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), | 103 | Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))), |
103 | () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE), | 104 | () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE), |
104 | is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))), | 105 | Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))), |
105 | () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE), | 106 | () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE), |
106 | is(new InferredType(Set.of(), Set.of(c3, c4), null))), | 107 | Matchers.is(new InferredType(Set.of(), Set.of(c3, c4), null))), |
107 | () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE), | 108 | () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE), |
108 | is(new InferredType(Set.of(), Set.of(c1, c4), null))), | 109 | Matchers.is(new InferredType(Set.of(), Set.of(c1, c4), null))), |
109 | () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE), | 110 | () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE), |
110 | is(new InferredType(Set.of(), Set.of(c3), null))) | 111 | Matchers.is(new InferredType(Set.of(), Set.of(c3), null))) |
111 | ); | 112 | ); |
112 | } | 113 | } |
113 | 114 | ||
@@ -117,8 +118,8 @@ class TypeAnalyzerExampleHierarchyTest { | |||
117 | var a4Result = tester.getPreservedType(a4); | 118 | var a4Result = tester.getPreservedType(a4); |
118 | var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null); | 119 | var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null); |
119 | assertAll( | 120 | assertAll( |
120 | () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), is(expected)), | 121 | () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected)), |
121 | () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), is(expected)) | 122 | () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected)) |
122 | ); | 123 | ); |
123 | } | 124 | } |
124 | 125 | ||
@@ -140,9 +141,9 @@ class TypeAnalyzerExampleHierarchyTest { | |||
140 | var c3Result = tester.getPreservedType(c3); | 141 | var c3Result = tester.getPreservedType(c3); |
141 | assertAll( | 142 | assertAll( |
142 | () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE), | 143 | () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE), |
143 | is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))), | 144 | Matchers.is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))), |
144 | () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), | 145 | () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), |
145 | is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null))) | 146 | Matchers.is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null))) |
146 | ); | 147 | ); |
147 | } | 148 | } |
148 | 149 | ||
@@ -153,13 +154,13 @@ class TypeAnalyzerExampleHierarchyTest { | |||
153 | var c1Result = tester.getPreservedType(c1); | 154 | var c1Result = tester.getPreservedType(c1); |
154 | assertAll( | 155 | assertAll( |
155 | () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | 156 | () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE), |
156 | is(new InferredType(Set.of(a1, a4), Set.of(), null))), | 157 | Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null))), |
157 | () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE), | 158 | () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE), |
158 | is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), | 159 | Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), |
159 | () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE), | 160 | () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE), |
160 | is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), | 161 | Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))), |
161 | () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | 162 | () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), |
162 | is(new InferredType(Set.of(a1, a4), Set.of(), null))) | 163 | Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null))) |
163 | ); | 164 | ); |
164 | } | 165 | } |
165 | 166 | ||
@@ -169,9 +170,9 @@ class TypeAnalyzerExampleHierarchyTest { | |||
169 | var a5Result = tester.getPreservedType(a5); | 170 | var a5Result = tester.getPreservedType(a5); |
170 | assertAll( | 171 | assertAll( |
171 | () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE), | 172 | () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE), |
172 | is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), | 173 | Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), |
173 | () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE), | 174 | () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE), |
174 | is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))) | 175 | Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))) |
175 | ); | 176 | ); |
176 | } | 177 | } |
177 | 178 | ||
@@ -193,9 +194,9 @@ class TypeAnalyzerExampleHierarchyTest { | |||
193 | var a5Result = tester.getPreservedType(a5); | 194 | var a5Result = tester.getPreservedType(a5); |
194 | assertAll( | 195 | assertAll( |
195 | () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR), | 196 | () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR), |
196 | is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), | 197 | Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), |
197 | () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR), | 198 | () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR), |
198 | is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), | 199 | Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))), |
199 | () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR), | 200 | () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR), |
200 | is(a5Result.asInferredType())) | 201 | is(a5Result.asInferredType())) |
201 | ); | 202 | ); |
diff --git a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java index 02903026..1aab75bb 100644 --- a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java +++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java | |||
@@ -1,5 +1,6 @@ | |||
1 | package tools.refinery.store.partial.translator.typehierarchy; | 1 | package tools.refinery.store.partial.translator.typehierarchy; |
2 | 2 | ||
3 | import org.hamcrest.Matchers; | ||
3 | import org.junit.jupiter.api.Test; | 4 | import org.junit.jupiter.api.Test; |
4 | import tools.refinery.store.partial.representation.PartialRelation; | 5 | import tools.refinery.store.partial.representation.PartialRelation; |
5 | import tools.refinery.store.representation.TruthValue; | 6 | import tools.refinery.store.representation.TruthValue; |
@@ -136,8 +137,8 @@ class TypeAnalyzerTest { | |||
136 | 137 | ||
137 | var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3); | 138 | var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3); |
138 | assertAll( | 139 | assertAll( |
139 | () -> assertThat(tester.getInferredType(c3), is(expected)), | 140 | () -> assertThat(tester.getInferredType(c3), Matchers.is(expected)), |
140 | () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(expected)) | 141 | () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), Matchers.is(expected)) |
141 | ); | 142 | ); |
142 | } | 143 | } |
143 | 144 | ||
@@ -161,7 +162,7 @@ class TypeAnalyzerTest { | |||
161 | var a1Result = tester.getPreservedType(a1); | 162 | var a1Result = tester.getPreservedType(a1); |
162 | 163 | ||
163 | assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | 164 | assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), |
164 | is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2))); | 165 | Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2))); |
165 | } | 166 | } |
166 | 167 | ||
167 | @Test | 168 | @Test |
@@ -184,7 +185,7 @@ class TypeAnalyzerTest { | |||
184 | var a1Result = tester.getPreservedType(a1); | 185 | var a1Result = tester.getPreservedType(a1); |
185 | 186 | ||
186 | assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), | 187 | assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE), |
187 | is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3))); | 188 | Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3))); |
188 | } | 189 | } |
189 | 190 | ||
190 | @Test | 191 | @Test |
diff --git a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java index ce600ea6..ce600ea6 100644 --- a/subprojects/store/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java +++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTester.java | |||
diff --git a/subprojects/store-query-viatra/build.gradle b/subprojects/store-query-viatra/build.gradle index c12b48fe..13a7544f 100644 --- a/subprojects/store-query-viatra/build.gradle +++ b/subprojects/store-query-viatra/build.gradle | |||
@@ -10,7 +10,7 @@ configurations.testRuntimeClasspath { | |||
10 | dependencies { | 10 | dependencies { |
11 | implementation libs.ecore | 11 | implementation libs.ecore |
12 | api libs.viatra | 12 | api libs.viatra |
13 | api project(':refinery-store') | 13 | api project(':refinery-store-query') |
14 | testImplementation libs.slf4j.simple | 14 | testImplementation libs.slf4j.simple |
15 | testImplementation libs.slf4j.log4j | 15 | testImplementation libs.slf4j.log4j |
16 | } | 16 | } |
diff --git a/subprojects/store-query/build.gradle b/subprojects/store-query/build.gradle new file mode 100644 index 00000000..2b76e608 --- /dev/null +++ b/subprojects/store-query/build.gradle | |||
@@ -0,0 +1,7 @@ | |||
1 | plugins { | ||
2 | id 'refinery-java-library' | ||
3 | } | ||
4 | |||
5 | dependencies { | ||
6 | api project(':refinery-store') | ||
7 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java new file mode 100644 index 00000000..760b264b --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java | |||
@@ -0,0 +1,112 @@ | |||
1 | package tools.refinery.store.query; | ||
2 | |||
3 | import tools.refinery.store.query.literal.CallPolarity; | ||
4 | import tools.refinery.store.query.literal.DnfCallLiteral; | ||
5 | import tools.refinery.store.query.literal.LiteralReduction; | ||
6 | |||
7 | import java.util.*; | ||
8 | |||
9 | public final class Dnf implements RelationLike { | ||
10 | private final String name; | ||
11 | |||
12 | private final String uniqueName; | ||
13 | |||
14 | private final List<Variable> parameters; | ||
15 | |||
16 | private final List<FunctionalDependency<Variable>> functionalDependencies; | ||
17 | |||
18 | private final List<DnfClause> clauses; | ||
19 | |||
20 | Dnf(String name, List<Variable> parameters, List<FunctionalDependency<Variable>> functionalDependencies, | ||
21 | List<DnfClause> clauses) { | ||
22 | validateFunctionalDependencies(parameters, functionalDependencies); | ||
23 | this.name = name; | ||
24 | this.uniqueName = DnfUtils.generateUniqueName(name); | ||
25 | this.parameters = parameters; | ||
26 | this.functionalDependencies = functionalDependencies; | ||
27 | this.clauses = clauses; | ||
28 | } | ||
29 | |||
30 | private static void validateFunctionalDependencies( | ||
31 | Collection<Variable> parameters, Collection<FunctionalDependency<Variable>> functionalDependencies) { | ||
32 | var parameterSet = new HashSet<>(parameters); | ||
33 | for (var functionalDependency : functionalDependencies) { | ||
34 | validateParameters(parameters, parameterSet, functionalDependency.forEach(), functionalDependency); | ||
35 | validateParameters(parameters, parameterSet, functionalDependency.unique(), functionalDependency); | ||
36 | } | ||
37 | } | ||
38 | |||
39 | private static void validateParameters(Collection<Variable> parameters, Set<Variable> parameterSet, | ||
40 | Collection<Variable> toValidate, | ||
41 | FunctionalDependency<Variable> functionalDependency) { | ||
42 | for (var variable : toValidate) { | ||
43 | if (!parameterSet.contains(variable)) { | ||
44 | throw new IllegalArgumentException( | ||
45 | "Variable %s of functional dependency %s does not appear in the parameter list %s" | ||
46 | .formatted(variable, functionalDependency, parameters)); | ||
47 | } | ||
48 | } | ||
49 | } | ||
50 | |||
51 | @Override | ||
52 | public String name() { | ||
53 | return name; | ||
54 | } | ||
55 | |||
56 | public String getUniqueName() { | ||
57 | return uniqueName; | ||
58 | } | ||
59 | |||
60 | public List<Variable> getParameters() { | ||
61 | return parameters; | ||
62 | } | ||
63 | |||
64 | public List<FunctionalDependency<Variable>> getFunctionalDependencies() { | ||
65 | return functionalDependencies; | ||
66 | } | ||
67 | |||
68 | @Override | ||
69 | public int arity() { | ||
70 | return parameters.size(); | ||
71 | } | ||
72 | |||
73 | public List<DnfClause> getClauses() { | ||
74 | return clauses; | ||
75 | } | ||
76 | |||
77 | public LiteralReduction getReduction() { | ||
78 | if (clauses.isEmpty()) { | ||
79 | return LiteralReduction.ALWAYS_FALSE; | ||
80 | } | ||
81 | for (var clause : clauses) { | ||
82 | if (clause.literals().isEmpty()) { | ||
83 | return LiteralReduction.ALWAYS_TRUE; | ||
84 | } | ||
85 | } | ||
86 | return LiteralReduction.NOT_REDUCIBLE; | ||
87 | } | ||
88 | |||
89 | public DnfCallLiteral call(CallPolarity polarity, List<Variable> arguments) { | ||
90 | return new DnfCallLiteral(polarity, this, arguments); | ||
91 | } | ||
92 | |||
93 | public DnfCallLiteral call(CallPolarity polarity, Variable... arguments) { | ||
94 | return call(polarity, List.of(arguments)); | ||
95 | } | ||
96 | |||
97 | public DnfCallLiteral call(Variable... arguments) { | ||
98 | return call(CallPolarity.POSITIVE, arguments); | ||
99 | } | ||
100 | |||
101 | public DnfCallLiteral callTransitive(Variable left, Variable right) { | ||
102 | return call(CallPolarity.TRANSITIVE, List.of(left, right)); | ||
103 | } | ||
104 | |||
105 | public static DnfBuilder builder() { | ||
106 | return builder(null); | ||
107 | } | ||
108 | |||
109 | public static DnfBuilder builder(String name) { | ||
110 | return new DnfBuilder(name); | ||
111 | } | ||
112 | } | ||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java new file mode 100644 index 00000000..b18b5177 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java | |||
@@ -0,0 +1,108 @@ | |||
1 | package tools.refinery.store.query; | ||
2 | |||
3 | import tools.refinery.store.query.literal.Literal; | ||
4 | |||
5 | import java.util.*; | ||
6 | |||
7 | @SuppressWarnings("UnusedReturnValue") | ||
8 | public class DnfBuilder { | ||
9 | private final String name; | ||
10 | |||
11 | private final List<Variable> parameters = new ArrayList<>(); | ||
12 | |||
13 | private final List<FunctionalDependency<Variable>> functionalDependencies = new ArrayList<>(); | ||
14 | |||
15 | private final List<List<Literal>> clauses = new ArrayList<>(); | ||
16 | |||
17 | DnfBuilder(String name) { | ||
18 | this.name = name; | ||
19 | } | ||
20 | |||
21 | public DnfBuilder parameter(Variable variable) { | ||
22 | parameters.add(variable); | ||
23 | return this; | ||
24 | } | ||
25 | |||
26 | public DnfBuilder parameters(Variable... variables) { | ||
27 | return parameters(List.of(variables)); | ||
28 | } | ||
29 | |||
30 | public DnfBuilder parameters(Collection<Variable> variables) { | ||
31 | parameters.addAll(variables); | ||
32 | return this; | ||
33 | } | ||
34 | |||
35 | public DnfBuilder functionalDependencies(Collection<FunctionalDependency<Variable>> functionalDependencies) { | ||
36 | this.functionalDependencies.addAll(functionalDependencies); | ||
37 | return this; | ||
38 | } | ||
39 | |||
40 | public DnfBuilder functionalDependency(FunctionalDependency<Variable> functionalDependency) { | ||
41 | functionalDependencies.add(functionalDependency); | ||
42 | return this; | ||
43 | } | ||
44 | |||
45 | public DnfBuilder functionalDependency(Set<Variable> forEach, Set<Variable> unique) { | ||
46 | return functionalDependency(new FunctionalDependency<>(forEach, unique)); | ||
47 | } | ||
48 | |||
49 | public DnfBuilder clause(Literal... literals) { | ||
50 | clause(List.of(literals)); | ||
51 | return this; | ||
52 | } | ||
53 | |||
54 | public DnfBuilder clause(Collection<Literal> literals) { | ||
55 | var filteredLiterals = new ArrayList<Literal>(literals.size()); | ||
56 | for (var literal : literals) { | ||
57 | var reduction = literal.getReduction(); | ||
58 | switch (reduction) { | ||
59 | case NOT_REDUCIBLE -> filteredLiterals.add(literal); | ||
60 | case ALWAYS_TRUE -> { | ||
61 | // Literals reducible to {@code true} can be omitted, because the model is always assumed to have at | ||
62 | // least on object. | ||
63 | } | ||
64 | case ALWAYS_FALSE -> { | ||
65 | // Clauses with {@code false} literals can be omitted entirely. | ||
66 | return this; | ||
67 | } | ||
68 | default -> throw new IllegalStateException("Invalid reduction %s".formatted(reduction)); | ||
69 | } | ||
70 | } | ||
71 | clauses.add(Collections.unmodifiableList(filteredLiterals)); | ||
72 | return this; | ||
73 | } | ||
74 | |||
75 | public DnfBuilder clause(DnfClause clause) { | ||
76 | return clause(clause.literals()); | ||
77 | } | ||
78 | |||
79 | public DnfBuilder clauses(DnfClause... clauses) { | ||
80 | for (var clause : clauses) { | ||
81 | this.clause(clause); | ||
82 | } | ||
83 | return this; | ||
84 | } | ||
85 | |||
86 | public DnfBuilder clauses(Collection<DnfClause> clauses) { | ||
87 | for (var clause : clauses) { | ||
88 | this.clause(clause); | ||
89 | } | ||
90 | return this; | ||
91 | } | ||
92 | |||
93 | public Dnf build() { | ||
94 | var postProcessedClauses = new ArrayList<DnfClause>(clauses.size()); | ||
95 | for (var constraints : clauses) { | ||
96 | var variables = new HashSet<Variable>(); | ||
97 | for (var constraint : constraints) { | ||
98 | constraint.collectAllVariables(variables); | ||
99 | } | ||
100 | parameters.forEach(variables::remove); | ||
101 | postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables), | ||
102 | Collections.unmodifiableList(constraints))); | ||
103 | } | ||
104 | return new Dnf(name, Collections.unmodifiableList(parameters), | ||
105 | Collections.unmodifiableList(functionalDependencies), | ||
106 | Collections.unmodifiableList(postProcessedClauses)); | ||
107 | } | ||
108 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/DnfClause.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java index 2ba6becc..2ba6becc 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/DnfClause.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java index 17564d43..17564d43 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/FunctionalDependency.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/FunctionalDependency.java index 63a81713..63a81713 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/FunctionalDependency.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/FunctionalDependency.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQuery.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQuery.java index 6a1aeabb..6a1aeabb 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQuery.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQuery.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java index f7762444..f7762444 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java index b3cfb4b4..b3cfb4b4 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java index 3efeacaa..091d6d06 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java | |||
@@ -1,8 +1,8 @@ | |||
1 | package tools.refinery.store.query; | 1 | package tools.refinery.store.query; |
2 | 2 | ||
3 | import tools.refinery.store.query.view.AnyRelationView; | ||
3 | import tools.refinery.store.adapter.ModelStoreAdapter; | 4 | import tools.refinery.store.adapter.ModelStoreAdapter; |
4 | import tools.refinery.store.model.Model; | 5 | import tools.refinery.store.model.Model; |
5 | import tools.refinery.store.query.view.AnyRelationView; | ||
6 | 6 | ||
7 | import java.util.Collection; | 7 | import java.util.Collection; |
8 | 8 | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/RelationLike.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/RelationLike.java index 8c784d8b..8c784d8b 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/RelationLike.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/RelationLike.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/ResultSet.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ResultSet.java index 3542e252..3542e252 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/ResultSet.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ResultSet.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java index 2eb87649..2eb87649 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java | |||
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java new file mode 100644 index 00000000..fd2f1eec --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java | |||
@@ -0,0 +1,37 @@ | |||
1 | package tools.refinery.store.query.literal; | ||
2 | |||
3 | import tools.refinery.store.query.Variable; | ||
4 | |||
5 | import java.util.Map; | ||
6 | import java.util.Set; | ||
7 | |||
8 | public class BooleanLiteral implements Literal { | ||
9 | public static final BooleanLiteral TRUE = new BooleanLiteral(LiteralReduction.ALWAYS_TRUE); | ||
10 | public static final BooleanLiteral FALSE = new BooleanLiteral(LiteralReduction.ALWAYS_FALSE); | ||
11 | |||
12 | private final LiteralReduction reduction; | ||
13 | |||
14 | private BooleanLiteral(LiteralReduction reduction) { | ||
15 | this.reduction = reduction; | ||
16 | } | ||
17 | |||
18 | @Override | ||
19 | public void collectAllVariables(Set<Variable> variables) { | ||
20 | // No variables to collect. | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public Literal substitute(Map<Variable, Variable> substitution) { | ||
25 | // No variables to substitute. | ||
26 | return this; | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | public LiteralReduction getReduction() { | ||
31 | return reduction; | ||
32 | } | ||
33 | |||
34 | public static BooleanLiteral fromBoolean(boolean value) { | ||
35 | return value ? TRUE : FALSE; | ||
36 | } | ||
37 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java index 5e1ae94d..5e1ae94d 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallPolarity.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallPolarity.java index 84b4b771..84b4b771 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallPolarity.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallPolarity.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java index 746d23af..746d23af 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java index 40499222..de6c6005 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java | |||
@@ -20,4 +20,10 @@ public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiter | |||
20 | public DnfCallLiteral negate() { | 20 | public DnfCallLiteral negate() { |
21 | return new DnfCallLiteral(getPolarity().negate(), getTarget(), getArguments()); | 21 | return new DnfCallLiteral(getPolarity().negate(), getTarget(), getArguments()); |
22 | } | 22 | } |
23 | |||
24 | @Override | ||
25 | public LiteralReduction getReduction() { | ||
26 | var dnfReduction = getTarget().getReduction(); | ||
27 | return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate(); | ||
28 | } | ||
23 | } | 29 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java index 5fee54b1..f30179b2 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java | |||
@@ -24,4 +24,12 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right | |||
24 | return new EquivalenceLiteral(positive, DnfUtils.maybeSubstitute(left, substitution), | 24 | return new EquivalenceLiteral(positive, DnfUtils.maybeSubstitute(left, substitution), |
25 | DnfUtils.maybeSubstitute(right, substitution)); | 25 | DnfUtils.maybeSubstitute(right, substitution)); |
26 | } | 26 | } |
27 | |||
28 | @Override | ||
29 | public LiteralReduction getReduction() { | ||
30 | if (left.equals(right)) { | ||
31 | return positive ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE; | ||
32 | } | ||
33 | return LiteralReduction.NOT_REDUCIBLE; | ||
34 | } | ||
27 | } | 35 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java index e0f5f605..a6893acf 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java | |||
@@ -9,4 +9,8 @@ public interface Literal { | |||
9 | void collectAllVariables(Set<Variable> variables); | 9 | void collectAllVariables(Set<Variable> variables); |
10 | 10 | ||
11 | Literal substitute(Map<Variable, Variable> substitution); | 11 | Literal substitute(Map<Variable, Variable> substitution); |
12 | |||
13 | default LiteralReduction getReduction() { | ||
14 | return LiteralReduction.NOT_REDUCIBLE; | ||
15 | } | ||
12 | } | 16 | } |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java new file mode 100644 index 00000000..146089f6 --- /dev/null +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java | |||
@@ -0,0 +1,26 @@ | |||
1 | package tools.refinery.store.query.literal; | ||
2 | |||
3 | public enum LiteralReduction { | ||
4 | /** | ||
5 | * Signifies that a literal should be preserved in the clause. | ||
6 | */ | ||
7 | NOT_REDUCIBLE, | ||
8 | |||
9 | /** | ||
10 | * Signifies that the literal may be omitted from the cause (if the model being queried is nonempty). | ||
11 | */ | ||
12 | ALWAYS_TRUE, | ||
13 | |||
14 | /** | ||
15 | * Signifies that the clause with the literal may be omitted entirely. | ||
16 | */ | ||
17 | ALWAYS_FALSE; | ||
18 | |||
19 | public LiteralReduction negate() { | ||
20 | return switch (this) { | ||
21 | case NOT_REDUCIBLE -> NOT_REDUCIBLE; | ||
22 | case ALWAYS_TRUE -> ALWAYS_FALSE; | ||
23 | case ALWAYS_FALSE -> ALWAYS_TRUE; | ||
24 | }; | ||
25 | } | ||
26 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literals.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java index 2c7e893f..2c7e893f 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literals.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java index 32523675..32523675 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java index 4718b550..4718b550 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/AnyRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java index 328cde3a..328cde3a 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/AnyRelationView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java index 64c601bb..64c601bb 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java index 3d278a8b..3d278a8b 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java index e1b2e45b..e1b2e45b 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java index 6accd27a..2714a8c5 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java | |||
@@ -1,8 +1,8 @@ | |||
1 | package tools.refinery.store.query.view; | 1 | package tools.refinery.store.query.view; |
2 | 2 | ||
3 | import tools.refinery.store.query.Variable; | ||
3 | import tools.refinery.store.map.CursorAsIterator; | 4 | import tools.refinery.store.map.CursorAsIterator; |
4 | import tools.refinery.store.model.Model; | 5 | import tools.refinery.store.model.Model; |
5 | import tools.refinery.store.query.Variable; | ||
6 | import tools.refinery.store.query.literal.CallPolarity; | 6 | import tools.refinery.store.query.literal.CallPolarity; |
7 | import tools.refinery.store.query.literal.RelationViewLiteral; | 7 | import tools.refinery.store.query.literal.RelationViewLiteral; |
8 | import tools.refinery.store.representation.Symbol; | 8 | import tools.refinery.store.representation.Symbol; |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java index 2ba1fcc4..2ba1fcc4 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java index 8cc4986e..8cc4986e 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java b/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java deleted file mode 100644 index 2c83a200..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java +++ /dev/null | |||
@@ -1,9 +0,0 @@ | |||
1 | package tools.refinery.store.partial; | ||
2 | |||
3 | import tools.refinery.store.adapter.ModelAdapter; | ||
4 | |||
5 | public interface PartialInterpretationAdapter extends ModelAdapter { | ||
6 | @Override | ||
7 | PartialInterpretationStoreAdapter getStoreAdapter(); | ||
8 | } | ||
9 | |||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java b/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java deleted file mode 100644 index 0ec13836..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java +++ /dev/null | |||
@@ -1,9 +0,0 @@ | |||
1 | package tools.refinery.store.partial; | ||
2 | |||
3 | import tools.refinery.store.adapter.ModelAdapterBuilder; | ||
4 | import tools.refinery.store.model.ModelStore; | ||
5 | |||
6 | public interface PartialInterpretationBuilder extends ModelAdapterBuilder { | ||
7 | @Override | ||
8 | PartialInterpretationStoreAdapter createStoreAdapter(ModelStore store); | ||
9 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java deleted file mode 100644 index b080094f..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java +++ /dev/null | |||
@@ -1,187 +0,0 @@ | |||
1 | package tools.refinery.store.query; | ||
2 | |||
3 | import tools.refinery.store.query.literal.CallPolarity; | ||
4 | import tools.refinery.store.query.literal.DnfCallLiteral; | ||
5 | import tools.refinery.store.query.literal.Literal; | ||
6 | |||
7 | import java.util.*; | ||
8 | |||
9 | public final class Dnf implements RelationLike { | ||
10 | private final String name; | ||
11 | |||
12 | private final String uniqueName; | ||
13 | |||
14 | private final List<Variable> parameters; | ||
15 | |||
16 | private final List<FunctionalDependency<Variable>> functionalDependencies; | ||
17 | |||
18 | private final List<DnfClause> clauses; | ||
19 | |||
20 | private Dnf(String name, List<Variable> parameters, List<FunctionalDependency<Variable>> functionalDependencies, | ||
21 | List<DnfClause> clauses) { | ||
22 | validateFunctionalDependencies(parameters, functionalDependencies); | ||
23 | this.name = name; | ||
24 | this.uniqueName = DnfUtils.generateUniqueName(name); | ||
25 | this.parameters = parameters; | ||
26 | this.functionalDependencies = functionalDependencies; | ||
27 | this.clauses = clauses; | ||
28 | } | ||
29 | |||
30 | private static void validateFunctionalDependencies( | ||
31 | Collection<Variable> parameters, Collection<FunctionalDependency<Variable>> functionalDependencies) { | ||
32 | var parameterSet = new HashSet<>(parameters); | ||
33 | for (var functionalDependency : functionalDependencies) { | ||
34 | validateParameters(parameters, parameterSet, functionalDependency.forEach(), functionalDependency); | ||
35 | validateParameters(parameters, parameterSet, functionalDependency.unique(), functionalDependency); | ||
36 | } | ||
37 | } | ||
38 | |||
39 | private static void validateParameters(Collection<Variable> parameters, Set<Variable> parameterSet, | ||
40 | Collection<Variable> toValidate, | ||
41 | FunctionalDependency<Variable> functionalDependency) { | ||
42 | for (var variable : toValidate) { | ||
43 | if (!parameterSet.contains(variable)) { | ||
44 | throw new IllegalArgumentException( | ||
45 | "Variable %s of functional dependency %s does not appear in the parameter list %s" | ||
46 | .formatted(variable, functionalDependency, parameters)); | ||
47 | } | ||
48 | } | ||
49 | } | ||
50 | |||
51 | @Override | ||
52 | public String name() { | ||
53 | return name; | ||
54 | } | ||
55 | |||
56 | public String getUniqueName() { | ||
57 | return uniqueName; | ||
58 | } | ||
59 | |||
60 | public List<Variable> getParameters() { | ||
61 | return parameters; | ||
62 | } | ||
63 | |||
64 | public List<FunctionalDependency<Variable>> getFunctionalDependencies() { | ||
65 | return functionalDependencies; | ||
66 | } | ||
67 | |||
68 | @Override | ||
69 | public int arity() { | ||
70 | return parameters.size(); | ||
71 | } | ||
72 | |||
73 | public List<DnfClause> getClauses() { | ||
74 | return clauses; | ||
75 | } | ||
76 | |||
77 | public DnfCallLiteral call(CallPolarity polarity, List<Variable> arguments) { | ||
78 | return new DnfCallLiteral(polarity, this, arguments); | ||
79 | } | ||
80 | |||
81 | public DnfCallLiteral call(CallPolarity polarity, Variable... arguments) { | ||
82 | return call(polarity, List.of(arguments)); | ||
83 | } | ||
84 | |||
85 | public DnfCallLiteral call(Variable... arguments) { | ||
86 | return call(CallPolarity.POSITIVE, arguments); | ||
87 | } | ||
88 | |||
89 | public DnfCallLiteral callTransitive(Variable left, Variable right) { | ||
90 | return call(CallPolarity.TRANSITIVE, List.of(left, right)); | ||
91 | } | ||
92 | |||
93 | public static Builder builder() { | ||
94 | return builder(null); | ||
95 | } | ||
96 | |||
97 | public static Builder builder(String name) { | ||
98 | return new Builder(name); | ||
99 | } | ||
100 | |||
101 | @SuppressWarnings("UnusedReturnValue") | ||
102 | public static class Builder { | ||
103 | private final String name; | ||
104 | |||
105 | private final List<Variable> parameters = new ArrayList<>(); | ||
106 | |||
107 | private final List<FunctionalDependency<Variable>> functionalDependencies = new ArrayList<>(); | ||
108 | |||
109 | private final List<List<Literal>> clauses = new ArrayList<>(); | ||
110 | |||
111 | private Builder(String name) { | ||
112 | this.name = name; | ||
113 | } | ||
114 | |||
115 | public Builder parameter(Variable variable) { | ||
116 | parameters.add(variable); | ||
117 | return this; | ||
118 | } | ||
119 | |||
120 | public Builder parameters(Variable... variables) { | ||
121 | return parameters(List.of(variables)); | ||
122 | } | ||
123 | |||
124 | public Builder parameters(Collection<Variable> variables) { | ||
125 | parameters.addAll(variables); | ||
126 | return this; | ||
127 | } | ||
128 | |||
129 | public Builder functionalDependencies(Collection<FunctionalDependency<Variable>> functionalDependencies) { | ||
130 | this.functionalDependencies.addAll(functionalDependencies); | ||
131 | return this; | ||
132 | } | ||
133 | |||
134 | public Builder functionalDependency(FunctionalDependency<Variable> functionalDependency) { | ||
135 | functionalDependencies.add(functionalDependency); | ||
136 | return this; | ||
137 | } | ||
138 | |||
139 | public Builder functionalDependency(Set<Variable> forEach, Set<Variable> unique) { | ||
140 | return functionalDependency(new FunctionalDependency<>(forEach, unique)); | ||
141 | } | ||
142 | |||
143 | public Builder clause(Literal... atoms) { | ||
144 | clauses.add(List.of(atoms)); | ||
145 | return this; | ||
146 | } | ||
147 | |||
148 | public Builder clause(Collection<Literal> atoms) { | ||
149 | clauses.add(List.copyOf(atoms)); | ||
150 | return this; | ||
151 | } | ||
152 | |||
153 | public Builder clause(DnfClause clause) { | ||
154 | return clause(clause.literals()); | ||
155 | } | ||
156 | |||
157 | public Builder clauses(DnfClause... clauses) { | ||
158 | for (var clause : clauses) { | ||
159 | this.clause(clause); | ||
160 | } | ||
161 | return this; | ||
162 | } | ||
163 | |||
164 | public Builder clauses(Collection<DnfClause> clauses) { | ||
165 | for (var clause : clauses) { | ||
166 | this.clause(clause); | ||
167 | } | ||
168 | return this; | ||
169 | } | ||
170 | |||
171 | public Dnf build() { | ||
172 | var postProcessedClauses = new ArrayList<DnfClause>(); | ||
173 | for (var constraints : clauses) { | ||
174 | var variables = new HashSet<Variable>(); | ||
175 | for (var constraint : constraints) { | ||
176 | constraint.collectAllVariables(variables); | ||
177 | } | ||
178 | parameters.forEach(variables::remove); | ||
179 | postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables), | ||
180 | Collections.unmodifiableList(constraints))); | ||
181 | } | ||
182 | return new Dnf(name, Collections.unmodifiableList(parameters), | ||
183 | Collections.unmodifiableList(functionalDependencies), | ||
184 | Collections.unmodifiableList(postProcessedClauses)); | ||
185 | } | ||
186 | } | ||
187 | } | ||