diff options
Diffstat (limited to 'subprojects/store-reasoning/src/main/java/tools')
28 files changed, 825 insertions, 196 deletions
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java index 6d416436..f560c74c 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java | |||
@@ -8,7 +8,9 @@ package tools.refinery.store.reasoning; | |||
8 | import tools.refinery.store.adapter.ModelAdapterBuilder; | 8 | import tools.refinery.store.adapter.ModelAdapterBuilder; |
9 | import tools.refinery.store.model.ModelStore; | 9 | import tools.refinery.store.model.ModelStore; |
10 | import tools.refinery.store.query.dnf.Dnf; | 10 | import tools.refinery.store.query.dnf.Dnf; |
11 | import tools.refinery.store.query.dnf.FunctionalQuery; | ||
11 | import tools.refinery.store.query.dnf.Query; | 12 | import tools.refinery.store.query.dnf.Query; |
13 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
12 | import tools.refinery.store.reasoning.literal.Concreteness; | 14 | import tools.refinery.store.reasoning.literal.Concreteness; |
13 | import tools.refinery.store.reasoning.literal.Modality; | 15 | import tools.refinery.store.reasoning.literal.Modality; |
14 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | 16 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; |
@@ -18,8 +20,6 @@ import tools.refinery.store.representation.Symbol; | |||
18 | 20 | ||
19 | @SuppressWarnings("UnusedReturnValue") | 21 | @SuppressWarnings("UnusedReturnValue") |
20 | public interface ReasoningBuilder extends ModelAdapterBuilder { | 22 | public interface ReasoningBuilder extends ModelAdapterBuilder { |
21 | ReasoningBuilder initialNodeCount(int nodeCount); | ||
22 | |||
23 | ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator); | 23 | ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator); |
24 | 24 | ||
25 | <T> ReasoningBuilder storageRefiner(Symbol<T> symbol, StorageRefiner.Factory<T> refiner); | 25 | <T> ReasoningBuilder storageRefiner(Symbol<T> symbol, StorageRefiner.Factory<T> refiner); |
@@ -28,6 +28,10 @@ public interface ReasoningBuilder extends ModelAdapterBuilder { | |||
28 | 28 | ||
29 | <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query); | 29 | <T> Query<T> lift(Modality modality, Concreteness concreteness, Query<T> query); |
30 | 30 | ||
31 | RelationalQuery lift(Modality modality, Concreteness concreteness, RelationalQuery query); | ||
32 | |||
33 | <T> FunctionalQuery<T> lift(Modality modality, Concreteness concreteness, FunctionalQuery<T> query); | ||
34 | |||
31 | Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf); | 35 | Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf); |
32 | 36 | ||
33 | @Override | 37 | @Override |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java index fae60d9e..6f9354eb 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java | |||
@@ -8,6 +8,7 @@ package tools.refinery.store.reasoning; | |||
8 | import tools.refinery.store.adapter.ModelStoreAdapter; | 8 | import tools.refinery.store.adapter.ModelStoreAdapter; |
9 | import tools.refinery.store.model.Model; | 9 | import tools.refinery.store.model.Model; |
10 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 10 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
11 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
11 | 12 | ||
12 | import java.util.Collection; | 13 | import java.util.Collection; |
13 | 14 | ||
@@ -16,7 +17,7 @@ public interface ReasoningStoreAdapter extends ModelStoreAdapter { | |||
16 | 17 | ||
17 | Collection<AnyPartialSymbol> getRefinablePartialSymbols(); | 18 | Collection<AnyPartialSymbol> getRefinablePartialSymbols(); |
18 | 19 | ||
19 | Model createInitialModel(); | 20 | Model createInitialModel(ModelSeed modelSeed); |
20 | 21 | ||
21 | @Override | 22 | @Override |
22 | ReasoningAdapter createModelAdapter(Model model); | 23 | ReasoningAdapter createModelAdapter(Model model); |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java new file mode 100644 index 00000000..bc379c64 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java | |||
@@ -0,0 +1,91 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.internal; | ||
7 | |||
8 | import tools.refinery.store.query.dnf.Dnf; | ||
9 | import tools.refinery.store.query.dnf.DnfClause; | ||
10 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
11 | import tools.refinery.store.query.literal.Literal; | ||
12 | import tools.refinery.store.query.term.Variable; | ||
13 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
14 | import tools.refinery.store.reasoning.literal.ModalConstraint; | ||
15 | import tools.refinery.store.reasoning.literal.Modality; | ||
16 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
17 | |||
18 | import java.util.*; | ||
19 | |||
20 | class PartialClauseRewriter { | ||
21 | private final PartialQueryRewriter rewriter; | ||
22 | private final List<Literal> completedLiterals = new ArrayList<>(); | ||
23 | private final Deque<Literal> workList = new ArrayDeque<>(); | ||
24 | private final Set<Variable> positiveVariables = new LinkedHashSet<>(); | ||
25 | private final Set<Variable> unmodifiablePositiveVariables = Collections.unmodifiableSet(positiveVariables); | ||
26 | |||
27 | public PartialClauseRewriter(PartialQueryRewriter rewriter) { | ||
28 | this.rewriter = rewriter; | ||
29 | } | ||
30 | |||
31 | public List<Literal> rewriteClause(DnfClause clause) { | ||
32 | workList.addAll(clause.literals()); | ||
33 | while (!workList.isEmpty()) { | ||
34 | var literal = workList.removeFirst(); | ||
35 | rewrite(literal); | ||
36 | } | ||
37 | return completedLiterals; | ||
38 | } | ||
39 | |||
40 | private void rewrite(Literal literal) { | ||
41 | if (!(literal instanceof AbstractCallLiteral callLiteral)) { | ||
42 | markAsDone(literal); | ||
43 | return; | ||
44 | } | ||
45 | var target = callLiteral.getTarget(); | ||
46 | if (target instanceof Dnf dnf) { | ||
47 | rewriteRecursively(callLiteral, dnf); | ||
48 | } else if (target instanceof ModalConstraint modalConstraint) { | ||
49 | var modality = modalConstraint.modality(); | ||
50 | var concreteness = modalConstraint.concreteness(); | ||
51 | var constraint = modalConstraint.constraint(); | ||
52 | if (constraint instanceof Dnf dnf) { | ||
53 | rewriteRecursively(callLiteral, modality, concreteness, dnf); | ||
54 | } else if (constraint instanceof PartialRelation partialRelation) { | ||
55 | rewrite(callLiteral, modality, concreteness, partialRelation); | ||
56 | } else { | ||
57 | throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint); | ||
58 | } | ||
59 | } else { | ||
60 | markAsDone(literal); | ||
61 | } | ||
62 | } | ||
63 | |||
64 | private void markAsDone(Literal literal) { | ||
65 | completedLiterals.add(literal); | ||
66 | positiveVariables.addAll(literal.getOutputVariables()); | ||
67 | } | ||
68 | |||
69 | private void rewriteRecursively(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, | ||
70 | Dnf dnf) { | ||
71 | var liftedDnf = rewriter.getLifter().lift(modality, concreteness, dnf); | ||
72 | rewriteRecursively(callLiteral, liftedDnf); | ||
73 | } | ||
74 | |||
75 | private void rewriteRecursively(AbstractCallLiteral callLiteral, Dnf dnf) { | ||
76 | var rewrittenDnf = rewriter.rewrite(dnf); | ||
77 | var rewrittenLiteral = callLiteral.withTarget(rewrittenDnf); | ||
78 | completedLiterals.add(rewrittenLiteral); | ||
79 | } | ||
80 | |||
81 | private void rewrite(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, | ||
82 | PartialRelation partialRelation) { | ||
83 | var relationRewriter = rewriter.getRelationRewriter(partialRelation); | ||
84 | var literals = relationRewriter.rewriteLiteral( | ||
85 | unmodifiablePositiveVariables, callLiteral, modality, concreteness); | ||
86 | int length = literals.size(); | ||
87 | for (int i = length - 1; i >= 0; i--) { | ||
88 | workList.addFirst(literals.get(i)); | ||
89 | } | ||
90 | } | ||
91 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java index 132022d1..79cba263 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialQueryRewriter.java | |||
@@ -6,18 +6,13 @@ | |||
6 | package tools.refinery.store.reasoning.internal; | 6 | package tools.refinery.store.reasoning.internal; |
7 | 7 | ||
8 | import tools.refinery.store.query.dnf.Dnf; | 8 | import tools.refinery.store.query.dnf.Dnf; |
9 | import tools.refinery.store.query.dnf.DnfClause; | ||
10 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
11 | import tools.refinery.store.query.literal.Literal; | ||
12 | import tools.refinery.store.query.rewriter.AbstractRecursiveRewriter; | 9 | import tools.refinery.store.query.rewriter.AbstractRecursiveRewriter; |
13 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; | 10 | import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter; |
14 | import tools.refinery.store.reasoning.lifting.DnfLifter; | 11 | import tools.refinery.store.reasoning.lifting.DnfLifter; |
15 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
16 | import tools.refinery.store.reasoning.literal.ModalConstraint; | ||
17 | import tools.refinery.store.reasoning.literal.Modality; | ||
18 | import tools.refinery.store.reasoning.representation.PartialRelation; | 12 | import tools.refinery.store.reasoning.representation.PartialRelation; |
19 | 13 | ||
20 | import java.util.*; | 14 | import java.util.HashMap; |
15 | import java.util.Map; | ||
21 | 16 | ||
22 | class PartialQueryRewriter extends AbstractRecursiveRewriter { | 17 | class PartialQueryRewriter extends AbstractRecursiveRewriter { |
23 | private final DnfLifter lifter; | 18 | private final DnfLifter lifter; |
@@ -27,6 +22,18 @@ class PartialQueryRewriter extends AbstractRecursiveRewriter { | |||
27 | this.lifter = lifter; | 22 | this.lifter = lifter; |
28 | } | 23 | } |
29 | 24 | ||
25 | DnfLifter getLifter() { | ||
26 | return lifter; | ||
27 | } | ||
28 | |||
29 | PartialRelationRewriter getRelationRewriter(PartialRelation partialRelation) { | ||
30 | var rewriter = relationRewriterMap.get(partialRelation); | ||
31 | if (rewriter == null) { | ||
32 | throw new IllegalArgumentException("Do not know how to interpret partial relation: " + partialRelation); | ||
33 | } | ||
34 | return rewriter; | ||
35 | } | ||
36 | |||
30 | public void addRelationRewriter(PartialRelation partialRelation, PartialRelationRewriter interpreter) { | 37 | public void addRelationRewriter(PartialRelation partialRelation, PartialRelationRewriter interpreter) { |
31 | if (relationRewriterMap.put(partialRelation, interpreter) != null) { | 38 | if (relationRewriterMap.put(partialRelation, interpreter) != null) { |
32 | throw new IllegalArgumentException("Duplicate partial relation: " + partialRelation); | 39 | throw new IllegalArgumentException("Duplicate partial relation: " + partialRelation); |
@@ -37,67 +44,10 @@ class PartialQueryRewriter extends AbstractRecursiveRewriter { | |||
37 | protected Dnf doRewrite(Dnf dnf) { | 44 | protected Dnf doRewrite(Dnf dnf) { |
38 | var builder = Dnf.builderFrom(dnf); | 45 | var builder = Dnf.builderFrom(dnf); |
39 | for (var clause : dnf.getClauses()) { | 46 | for (var clause : dnf.getClauses()) { |
40 | builder.clause(rewriteClause(clause)); | 47 | var clauseRewriter = new PartialClauseRewriter(this); |
48 | var rewrittenClauses = clauseRewriter.rewriteClause(clause); | ||
49 | builder.clause(rewrittenClauses); | ||
41 | } | 50 | } |
42 | return builder.build(); | 51 | return builder.build(); |
43 | } | 52 | } |
44 | |||
45 | private List<Literal> rewriteClause(DnfClause clause) { | ||
46 | var completedLiterals = new ArrayList<Literal>(); | ||
47 | var workList = new ArrayDeque<>(clause.literals()); | ||
48 | while (!workList.isEmpty()) { | ||
49 | var literal = workList.removeFirst(); | ||
50 | rewrite(literal, completedLiterals, workList); | ||
51 | } | ||
52 | return completedLiterals; | ||
53 | } | ||
54 | |||
55 | private void rewrite(Literal literal, List<Literal> completedLiterals, Deque<Literal> workList) { | ||
56 | if (!(literal instanceof AbstractCallLiteral callLiteral)) { | ||
57 | completedLiterals.add(literal); | ||
58 | return; | ||
59 | } | ||
60 | var target = callLiteral.getTarget(); | ||
61 | if (target instanceof Dnf dnf) { | ||
62 | rewriteRecursively(callLiteral, dnf, completedLiterals); | ||
63 | } else if (target instanceof ModalConstraint modalConstraint) { | ||
64 | var modality = modalConstraint.modality(); | ||
65 | var concreteness = modalConstraint.concreteness(); | ||
66 | var constraint = modalConstraint.constraint(); | ||
67 | if (constraint instanceof Dnf dnf) { | ||
68 | rewriteRecursively(callLiteral, modality, concreteness, dnf, completedLiterals); | ||
69 | } else if (constraint instanceof PartialRelation partialRelation) { | ||
70 | rewrite(callLiteral, modality, concreteness, partialRelation, workList); | ||
71 | } else { | ||
72 | throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint); | ||
73 | } | ||
74 | } else { | ||
75 | completedLiterals.add(literal); | ||
76 | } | ||
77 | } | ||
78 | |||
79 | private void rewriteRecursively(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, | ||
80 | Dnf dnf, List<Literal> completedLiterals) { | ||
81 | var liftedDnf = lifter.lift(modality, concreteness, dnf); | ||
82 | rewriteRecursively(callLiteral, liftedDnf, completedLiterals); | ||
83 | } | ||
84 | |||
85 | private void rewriteRecursively(AbstractCallLiteral callLiteral, Dnf dnf, List<Literal> completedLiterals) { | ||
86 | var rewrittenDnf = rewrite(dnf); | ||
87 | var rewrittenLiteral = callLiteral.withTarget(rewrittenDnf); | ||
88 | completedLiterals.add(rewrittenLiteral); | ||
89 | } | ||
90 | |||
91 | private void rewrite(AbstractCallLiteral callLiteral, Modality modality, Concreteness concreteness, | ||
92 | PartialRelation partialRelation, Deque<Literal> workList) { | ||
93 | var rewriter = relationRewriterMap.get(partialRelation); | ||
94 | if (rewriter == null) { | ||
95 | throw new IllegalArgumentException("Do not know how to interpret partial relation: " + partialRelation); | ||
96 | } | ||
97 | var literals = rewriter.rewriteLiteral(callLiteral, modality, concreteness); | ||
98 | int length = literals.size(); | ||
99 | for (int i = length - 1; i >= 0; i--) { | ||
100 | workList.addFirst(literals.get(i)); | ||
101 | } | ||
102 | } | ||
103 | } | 53 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java index 396c2dcc..579b08dd 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java | |||
@@ -48,7 +48,7 @@ class ReasoningAdapterImpl implements ReasoningAdapter { | |||
48 | refiners = new HashMap<>(refinerFactories.size()); | 48 | refiners = new HashMap<>(refinerFactories.size()); |
49 | createRefiners(); | 49 | createRefiners(); |
50 | 50 | ||
51 | storageRefiners = storeAdapter.createRepresentationRefiners(model); | 51 | storageRefiners = storeAdapter.createStprageRefiner(model); |
52 | 52 | ||
53 | nodeCountInterpretation = model.getInterpretation(NODE_COUNT_SYMBOL); | 53 | nodeCountInterpretation = model.getInterpretation(NODE_COUNT_SYMBOL); |
54 | } | 54 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java index f7a91284..2af84e2d 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java | |||
@@ -10,7 +10,9 @@ import tools.refinery.store.model.ModelStore; | |||
10 | import tools.refinery.store.model.ModelStoreBuilder; | 10 | import tools.refinery.store.model.ModelStoreBuilder; |
11 | import tools.refinery.store.query.ModelQueryBuilder; | 11 | import tools.refinery.store.query.ModelQueryBuilder; |
12 | import tools.refinery.store.query.dnf.Dnf; | 12 | import tools.refinery.store.query.dnf.Dnf; |
13 | import tools.refinery.store.query.dnf.FunctionalQuery; | ||
13 | import tools.refinery.store.query.dnf.Query; | 14 | import tools.refinery.store.query.dnf.Query; |
15 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
14 | import tools.refinery.store.reasoning.ReasoningBuilder; | 16 | import tools.refinery.store.reasoning.ReasoningBuilder; |
15 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | 17 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; |
16 | import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner; | 18 | import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner; |
@@ -38,16 +40,6 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningS | |||
38 | new LinkedHashMap<>(); | 40 | new LinkedHashMap<>(); |
39 | private final Map<AnySymbol, StorageRefiner.Factory<?>> registeredStorageRefiners = new LinkedHashMap<>(); | 41 | private final Map<AnySymbol, StorageRefiner.Factory<?>> registeredStorageRefiners = new LinkedHashMap<>(); |
40 | private final List<PartialModelInitializer> initializers = new ArrayList<>(); | 42 | private final List<PartialModelInitializer> initializers = new ArrayList<>(); |
41 | private int initialNodeCount = 0; | ||
42 | |||
43 | @Override | ||
44 | public ReasoningBuilder initialNodeCount(int nodeCount) { | ||
45 | if (nodeCount < 0) { | ||
46 | throw new IllegalArgumentException("Initial model size must not be negative"); | ||
47 | } | ||
48 | initialNodeCount = nodeCount; | ||
49 | return this; | ||
50 | } | ||
51 | 43 | ||
52 | @Override | 44 | @Override |
53 | public ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator) { | 45 | public ReasoningBuilder partialSymbol(AnyPartialSymbolTranslator translator) { |
@@ -81,6 +73,16 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningS | |||
81 | } | 73 | } |
82 | 74 | ||
83 | @Override | 75 | @Override |
76 | public RelationalQuery lift(Modality modality, Concreteness concreteness, RelationalQuery query) { | ||
77 | return lifter.lift(modality, concreteness, query); | ||
78 | } | ||
79 | |||
80 | @Override | ||
81 | public <T> FunctionalQuery<T> lift(Modality modality, Concreteness concreteness, FunctionalQuery<T> query) { | ||
82 | return lifter.lift(modality, concreteness, query); | ||
83 | } | ||
84 | |||
85 | @Override | ||
84 | public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { | 86 | public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { |
85 | return lifter.lift(modality, concreteness, dnf); | 87 | return lifter.lift(modality, concreteness, dnf); |
86 | } | 88 | } |
@@ -114,7 +116,7 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningS | |||
114 | 116 | ||
115 | @Override | 117 | @Override |
116 | public ReasoningStoreAdapterImpl doBuild(ModelStore store) { | 118 | public ReasoningStoreAdapterImpl doBuild(ModelStore store) { |
117 | return new ReasoningStoreAdapterImpl(store, initialNodeCount, Collections.unmodifiableMap(symbolInterpreters), | 119 | return new ReasoningStoreAdapterImpl(store, Collections.unmodifiableMap(symbolInterpreters), |
118 | Collections.unmodifiableMap(symbolRefiners), getStorageRefiners(store), | 120 | Collections.unmodifiableMap(symbolRefiners), getStorageRefiners(store), |
119 | Collections.unmodifiableList(initializers)); | 121 | Collections.unmodifiableList(initializers)); |
120 | } | 122 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java index e8b581c6..3dac53ef 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java | |||
@@ -14,6 +14,7 @@ import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | |||
14 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | 14 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; |
15 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | 15 | import tools.refinery.store.reasoning.refinement.StorageRefiner; |
16 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 16 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
17 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
17 | import tools.refinery.store.representation.AnySymbol; | 18 | import tools.refinery.store.representation.AnySymbol; |
18 | import tools.refinery.store.representation.Symbol; | 19 | import tools.refinery.store.representation.Symbol; |
19 | import tools.refinery.store.tuple.Tuple; | 20 | import tools.refinery.store.tuple.Tuple; |
@@ -26,23 +27,18 @@ class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { | |||
26 | private final ModelStore store; | 27 | private final ModelStore store; |
27 | private final Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters; | 28 | private final Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters; |
28 | private final Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners; | 29 | private final Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners; |
29 | private final Map<AnySymbol, StorageRefiner.Factory<?>> representationRefiners; | 30 | private final Map<AnySymbol, StorageRefiner.Factory<?>> storageRefiners; |
30 | private final Object initialModelLock = new Object(); | 31 | private final List<PartialModelInitializer> initializers; |
31 | private final int initialNodeCount; | ||
32 | private List<PartialModelInitializer> initializers; | ||
33 | private long initialCommitId = Model.NO_STATE_ID; | ||
34 | 32 | ||
35 | ReasoningStoreAdapterImpl(ModelStore store, | 33 | ReasoningStoreAdapterImpl(ModelStore store, |
36 | int initialNodeCount, | ||
37 | Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters, | 34 | Map<AnyPartialSymbol, PartialInterpretation.Factory<?, ?>> symbolInterpreters, |
38 | Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners, | 35 | Map<AnyPartialSymbol, PartialInterpretationRefiner.Factory<?, ?>> symbolRefiners, |
39 | Map<AnySymbol, StorageRefiner.Factory<?>> representationRefiners, | 36 | Map<AnySymbol, StorageRefiner.Factory<?>> storageRefiners, |
40 | List<PartialModelInitializer> initializers) { | 37 | List<PartialModelInitializer> initializers) { |
41 | this.store = store; | 38 | this.store = store; |
42 | this.initialNodeCount = initialNodeCount; | ||
43 | this.symbolInterpreters = symbolInterpreters; | 39 | this.symbolInterpreters = symbolInterpreters; |
44 | this.symbolRefiners = symbolRefiners; | 40 | this.symbolRefiners = symbolRefiners; |
45 | this.representationRefiners = representationRefiners; | 41 | this.storageRefiners = storageRefiners; |
46 | this.initializers = initializers; | 42 | this.initializers = initializers; |
47 | } | 43 | } |
48 | 44 | ||
@@ -73,44 +69,32 @@ class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { | |||
73 | return symbolRefiners; | 69 | return symbolRefiners; |
74 | } | 70 | } |
75 | 71 | ||
76 | StorageRefiner[] createRepresentationRefiners(Model model) { | 72 | StorageRefiner[] createStprageRefiner(Model model) { |
77 | var refiners = new StorageRefiner[representationRefiners.size()]; | 73 | var refiners = new StorageRefiner[storageRefiners.size()]; |
78 | int i = 0; | 74 | int i = 0; |
79 | for (var entry : representationRefiners.entrySet()) { | 75 | for (var entry : storageRefiners.entrySet()) { |
80 | var symbol = entry.getKey(); | 76 | var symbol = entry.getKey(); |
81 | var factory = entry.getValue(); | 77 | var factory = entry.getValue(); |
82 | refiners[i] = createRepresentationRefiner(factory, model, symbol); | 78 | refiners[i] = createStorageRefiner(factory, model, symbol); |
79 | i++; | ||
83 | } | 80 | } |
84 | return refiners; | 81 | return refiners; |
85 | } | 82 | } |
86 | 83 | ||
87 | private <T> StorageRefiner createRepresentationRefiner( | 84 | private <T> StorageRefiner createStorageRefiner(StorageRefiner.Factory<T> factory, Model model, AnySymbol symbol) { |
88 | StorageRefiner.Factory<T> factory, Model model, AnySymbol symbol) { | ||
89 | // The builder only allows well-typed assignment of refiners to symbols. | 85 | // The builder only allows well-typed assignment of refiners to symbols. |
90 | @SuppressWarnings("unchecked") | 86 | @SuppressWarnings("unchecked") |
91 | var typedSymbol = (Symbol<T>) symbol; | 87 | var typedSymbol = (Symbol<T>) symbol; |
92 | return factory.create(typedSymbol, model); | 88 | return factory.create(typedSymbol, model); |
93 | } | 89 | } |
94 | 90 | ||
95 | @Override | 91 | public Model createInitialModel(ModelSeed modelSeed) { |
96 | public Model createInitialModel() { | ||
97 | synchronized (initialModelLock) { | ||
98 | if (initialCommitId == Model.NO_STATE_ID) { | ||
99 | return doCreateInitialModel(); | ||
100 | } | ||
101 | return store.createModelForState(initialCommitId); | ||
102 | } | ||
103 | } | ||
104 | |||
105 | private Model doCreateInitialModel() { | ||
106 | var model = store.createEmptyModel(); | 92 | var model = store.createEmptyModel(); |
107 | model.getInterpretation(ReasoningAdapterImpl.NODE_COUNT_SYMBOL).put(Tuple.of(), initialNodeCount); | 93 | model.getInterpretation(ReasoningAdapterImpl.NODE_COUNT_SYMBOL).put(Tuple.of(), modelSeed.getNodeCount()); |
108 | for (var initializer : initializers) { | 94 | for (var initializer : initializers) { |
109 | initializer.initialize(model, initialNodeCount); | 95 | initializer.initialize(model, modelSeed); |
110 | } | 96 | } |
111 | model.getAdapter(ModelQueryAdapter.class).flushChanges(); | 97 | model.getAdapter(ModelQueryAdapter.class).flushChanges(); |
112 | initialCommitId = model.commit(); | ||
113 | initializers = null; | ||
114 | return model; | 98 | return model; |
115 | } | 99 | } |
116 | 100 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java index da8ae0a8..6ad35c20 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/PartialRelationRewriter.java | |||
@@ -7,11 +7,15 @@ package tools.refinery.store.reasoning.interpretation; | |||
7 | 7 | ||
8 | import tools.refinery.store.query.literal.AbstractCallLiteral; | 8 | import tools.refinery.store.query.literal.AbstractCallLiteral; |
9 | import tools.refinery.store.query.literal.Literal; | 9 | import tools.refinery.store.query.literal.Literal; |
10 | import tools.refinery.store.query.term.Variable; | ||
10 | import tools.refinery.store.reasoning.literal.Concreteness; | 11 | import tools.refinery.store.reasoning.literal.Concreteness; |
11 | import tools.refinery.store.reasoning.literal.Modality; | 12 | import tools.refinery.store.reasoning.literal.Modality; |
12 | 13 | ||
13 | import java.util.List; | 14 | import java.util.List; |
15 | import java.util.Set; | ||
14 | 16 | ||
17 | @FunctionalInterface | ||
15 | public interface PartialRelationRewriter { | 18 | public interface PartialRelationRewriter { |
16 | List<Literal> rewriteLiteral(AbstractCallLiteral literal, Modality modality, Concreteness concreteness); | 19 | List<Literal> rewriteLiteral(Set<Variable> positiveVariables, AbstractCallLiteral literal, Modality modality, |
20 | Concreteness concreteness); | ||
17 | } | 21 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java index 3be9e9ac..78fdbb89 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/interpretation/QueryBasedRelationRewriter.java | |||
@@ -5,30 +5,49 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.interpretation; | 6 | package tools.refinery.store.reasoning.interpretation; |
7 | 7 | ||
8 | import tools.refinery.store.query.dnf.Query; | 8 | import tools.refinery.store.query.dnf.RelationalQuery; |
9 | import tools.refinery.store.query.literal.AbstractCallLiteral; | 9 | import tools.refinery.store.query.literal.AbstractCallLiteral; |
10 | import tools.refinery.store.query.literal.Literal; | 10 | import tools.refinery.store.query.literal.Literal; |
11 | import tools.refinery.store.query.term.Variable; | ||
11 | import tools.refinery.store.reasoning.literal.Concreteness; | 12 | import tools.refinery.store.reasoning.literal.Concreteness; |
12 | import tools.refinery.store.reasoning.literal.Modality; | 13 | import tools.refinery.store.reasoning.literal.Modality; |
13 | 14 | ||
14 | import java.util.List; | 15 | import java.util.List; |
16 | import java.util.Set; | ||
15 | 17 | ||
16 | public class QueryBasedRelationRewriter implements PartialRelationRewriter { | 18 | public class QueryBasedRelationRewriter implements PartialRelationRewriter { |
17 | private final Query<Boolean> may; | 19 | private final RelationalQuery may; |
18 | private final Query<Boolean> must; | 20 | private final RelationalQuery must; |
19 | private final Query<Boolean> candidateMay; | 21 | private final RelationalQuery candidateMay; |
20 | private final Query<Boolean> candidateMust; | 22 | private final RelationalQuery candidateMust; |
21 | 23 | ||
22 | public QueryBasedRelationRewriter(Query<Boolean> may, Query<Boolean> must, Query<Boolean> candidateMay, | 24 | public QueryBasedRelationRewriter(RelationalQuery may, RelationalQuery must, RelationalQuery candidateMay, |
23 | Query<Boolean> candidateMust) { | 25 | RelationalQuery candidateMust) { |
24 | this.may = may; | 26 | this.may = may; |
25 | this.must = must; | 27 | this.must = must; |
26 | this.candidateMay = candidateMay; | 28 | this.candidateMay = candidateMay; |
27 | this.candidateMust = candidateMust; | 29 | this.candidateMust = candidateMust; |
28 | } | 30 | } |
29 | 31 | ||
32 | public RelationalQuery getMay() { | ||
33 | return may; | ||
34 | } | ||
35 | |||
36 | public RelationalQuery getMust() { | ||
37 | return must; | ||
38 | } | ||
39 | |||
40 | public RelationalQuery getCandidateMay() { | ||
41 | return candidateMay; | ||
42 | } | ||
43 | |||
44 | public RelationalQuery getCandidateMust() { | ||
45 | return candidateMust; | ||
46 | } | ||
47 | |||
30 | @Override | 48 | @Override |
31 | public List<Literal> rewriteLiteral(AbstractCallLiteral literal, Modality modality, Concreteness concreteness) { | 49 | public List<Literal> rewriteLiteral(Set<Variable> positiveVariables, AbstractCallLiteral literal, |
50 | Modality modality, Concreteness concreteness) { | ||
32 | var query = switch (concreteness) { | 51 | var query = switch (concreteness) { |
33 | case PARTIAL -> switch (modality) { | 52 | case PARTIAL -> switch (modality) { |
34 | case MAY -> may; | 53 | case MAY -> may; |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java index 2e68fa3e..6ac3efc0 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java | |||
@@ -5,9 +5,7 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.lifting; | 6 | package tools.refinery.store.reasoning.lifting; |
7 | 7 | ||
8 | import tools.refinery.store.query.dnf.Dnf; | 8 | import tools.refinery.store.query.dnf.*; |
9 | import tools.refinery.store.query.dnf.DnfClause; | ||
10 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.query.equality.DnfEqualityChecker; | 9 | import tools.refinery.store.query.equality.DnfEqualityChecker; |
12 | import tools.refinery.store.query.literal.Literal; | 10 | import tools.refinery.store.query.literal.Literal; |
13 | import tools.refinery.store.reasoning.literal.Concreteness; | 11 | import tools.refinery.store.reasoning.literal.Concreteness; |
@@ -25,6 +23,16 @@ public class DnfLifter { | |||
25 | return query.withDnf(liftedDnf); | 23 | return query.withDnf(liftedDnf); |
26 | } | 24 | } |
27 | 25 | ||
26 | public <T> RelationalQuery lift(Modality modality, Concreteness concreteness, RelationalQuery query) { | ||
27 | var liftedDnf = lift(modality, concreteness, query.getDnf()); | ||
28 | return query.withDnf(liftedDnf); | ||
29 | } | ||
30 | |||
31 | public <T> FunctionalQuery<T> lift(Modality modality, Concreteness concreteness, FunctionalQuery<T> query) { | ||
32 | var liftedDnf = lift(modality, concreteness, query.getDnf()); | ||
33 | return query.withDnf(liftedDnf); | ||
34 | } | ||
35 | |||
28 | public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { | 36 | public Dnf lift(Modality modality, Concreteness concreteness, Dnf dnf) { |
29 | return cache.computeIfAbsent(new ModalDnf(modality, concreteness, dnf), this::doLift); | 37 | return cache.computeIfAbsent(new ModalDnf(modality, concreteness, dnf), this::doLift); |
30 | } | 38 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AbstractPartialInterpretationRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AbstractPartialInterpretationRefiner.java new file mode 100644 index 00000000..a7fc5b7e --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/AbstractPartialInterpretationRefiner.java | |||
@@ -0,0 +1,29 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.refinement; | ||
7 | |||
8 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
9 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
10 | |||
11 | public abstract class AbstractPartialInterpretationRefiner<A, C> implements PartialInterpretationRefiner<A, C> { | ||
12 | private final ReasoningAdapter adapter; | ||
13 | private final PartialSymbol<A, C> partialSymbol; | ||
14 | |||
15 | protected AbstractPartialInterpretationRefiner(ReasoningAdapter adapter, PartialSymbol<A, C> partialSymbol) { | ||
16 | this.adapter = adapter; | ||
17 | this.partialSymbol = partialSymbol; | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public ReasoningAdapter getAdapter() { | ||
22 | return adapter; | ||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public PartialSymbol<A, C> getPartialSymbol() { | ||
27 | return partialSymbol; | ||
28 | } | ||
29 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java index 756118a0..ebb9b824 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/ConcreteSymbolRefiner.java | |||
@@ -13,39 +13,26 @@ import tools.refinery.store.tuple.Tuple; | |||
13 | 13 | ||
14 | import java.util.Objects; | 14 | import java.util.Objects; |
15 | 15 | ||
16 | public class ConcreteSymbolRefiner<A, C> implements PartialInterpretationRefiner<A, C> { | 16 | public class ConcreteSymbolRefiner<A, C> extends AbstractPartialInterpretationRefiner<A, C> { |
17 | private final ReasoningAdapter adapter; | ||
18 | private final PartialSymbol<A, C> partialSymbol; | ||
19 | private final Interpretation<A> interpretation; | 17 | private final Interpretation<A> interpretation; |
20 | 18 | ||
21 | public ConcreteSymbolRefiner(ReasoningAdapter adapter, PartialSymbol<A, C> partialSymbol, | 19 | public ConcreteSymbolRefiner(ReasoningAdapter adapter, PartialSymbol<A, C> partialSymbol, |
22 | Symbol<A> concreteSymbol) { | 20 | Symbol<A> concreteSymbol) { |
23 | this.adapter = adapter; | 21 | super(adapter, partialSymbol); |
24 | this.partialSymbol = partialSymbol; | ||
25 | interpretation = adapter.getModel().getInterpretation(concreteSymbol); | 22 | interpretation = adapter.getModel().getInterpretation(concreteSymbol); |
26 | } | 23 | } |
27 | 24 | ||
28 | @Override | 25 | @Override |
29 | public ReasoningAdapter getAdapter() { | ||
30 | return adapter; | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public PartialSymbol<A, C> getPartialSymbol() { | ||
35 | return partialSymbol; | ||
36 | } | ||
37 | |||
38 | @Override | ||
39 | public boolean merge(Tuple key, A value) { | 26 | public boolean merge(Tuple key, A value) { |
40 | var currentValue = interpretation.get(key); | 27 | var currentValue = interpretation.get(key); |
41 | var mergedValue = partialSymbol.abstractDomain().commonRefinement(currentValue, value); | 28 | var mergedValue = getPartialSymbol().abstractDomain().commonRefinement(currentValue, value); |
42 | if (!Objects.equals(currentValue, mergedValue)) { | 29 | if (!Objects.equals(currentValue, mergedValue)) { |
43 | interpretation.put(key, mergedValue); | 30 | interpretation.put(key, mergedValue); |
44 | } | 31 | } |
45 | return true; | 32 | return true; |
46 | } | 33 | } |
47 | 34 | ||
48 | public static <A1, C1> PartialInterpretationRefiner.Factory<A1, C1> of(Symbol<A1> concreteSymbol) { | 35 | public static <A1, C1> Factory<A1, C1> of(Symbol<A1> concreteSymbol) { |
49 | return (adapter, partialSymbol) -> new ConcreteSymbolRefiner<>(adapter, partialSymbol, concreteSymbol); | 36 | return (adapter, partialSymbol) -> new ConcreteSymbolRefiner<>(adapter, partialSymbol, concreteSymbol); |
50 | } | 37 | } |
51 | } | 38 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java index 0d7d6c5c..d4ec2e8b 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/DefaultStorageRefiner.java | |||
@@ -6,18 +6,17 @@ | |||
6 | package tools.refinery.store.reasoning.refinement; | 6 | package tools.refinery.store.reasoning.refinement; |
7 | 7 | ||
8 | import tools.refinery.store.model.Interpretation; | 8 | import tools.refinery.store.model.Interpretation; |
9 | import tools.refinery.store.model.Model; | ||
10 | import tools.refinery.store.representation.Symbol; | ||
9 | import tools.refinery.store.tuple.Tuple; | 11 | import tools.refinery.store.tuple.Tuple; |
10 | 12 | ||
11 | public class DefaultStorageRefiner<T> implements StorageRefiner { | 13 | public class DefaultStorageRefiner<T> implements StorageRefiner { |
12 | private static final StorageRefiner.Factory<Object> FACTORY = (symbol, model) -> { | 14 | private static final StorageRefiner.Factory<Object> FACTORY = DefaultStorageRefiner::new; |
13 | var interpretation = model.getInterpretation(symbol); | ||
14 | return new DefaultStorageRefiner<>(interpretation); | ||
15 | }; | ||
16 | 15 | ||
17 | private final Interpretation<T> interpretation; | 16 | private final Interpretation<T> interpretation; |
18 | 17 | ||
19 | public DefaultStorageRefiner(Interpretation<T> interpretation) { | 18 | public DefaultStorageRefiner(Symbol<T> symbol, Model model) { |
20 | this.interpretation = interpretation; | 19 | interpretation = model.getInterpretation(symbol); |
21 | } | 20 | } |
22 | 21 | ||
23 | @Override | 22 | @Override |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java index 79c1670f..0c82695c 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/PartialModelInitializer.java | |||
@@ -6,8 +6,9 @@ | |||
6 | package tools.refinery.store.reasoning.refinement; | 6 | package tools.refinery.store.reasoning.refinement; |
7 | 7 | ||
8 | import tools.refinery.store.model.Model; | 8 | import tools.refinery.store.model.Model; |
9 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
9 | 10 | ||
10 | @FunctionalInterface | 11 | @FunctionalInterface |
11 | public interface PartialModelInitializer { | 12 | public interface PartialModelInitializer { |
12 | void initialize(Model model, int nodeCount); | 13 | void initialize(Model model, ModelSeed modelSeed); |
13 | } | 14 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java index b5a3d844..8b1c3bb3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java | |||
@@ -75,7 +75,7 @@ record MapBasedSeed<T>(int arity, Class<T> valueType, T reducedValue, Map<Tuple, | |||
75 | private boolean moveToNext() { | 75 | private boolean moveToNext() { |
76 | do { | 76 | do { |
77 | increment(); | 77 | increment(); |
78 | } while (!checkValue()); | 78 | } while (state != State.TERMINATED && !checkValue()); |
79 | return state != State.TERMINATED; | 79 | return state != State.TERMINATED; |
80 | } | 80 | } |
81 | 81 | ||
@@ -89,16 +89,10 @@ record MapBasedSeed<T>(int arity, Class<T> valueType, T reducedValue, Map<Tuple, | |||
89 | counter[i] = 0; | 89 | counter[i] = 0; |
90 | i--; | 90 | i--; |
91 | } | 91 | } |
92 | state = State.TERMINATED; | ||
92 | } | 93 | } |
93 | 94 | ||
94 | private boolean checkValue() { | 95 | private boolean checkValue() { |
95 | if (state == State.TERMINATED) { | ||
96 | return false; | ||
97 | } | ||
98 | if (counter[0] >= nodeCount) { | ||
99 | state = State.TERMINATED; | ||
100 | return false; | ||
101 | } | ||
102 | key = Tuple.of(counter); | 96 | key = Tuple.of(counter); |
103 | var valueInMap = map.get(key); | 97 | var valueInMap = map.get(key); |
104 | if (Objects.equals(valueInMap, defaultValue)) { | 98 | if (Objects.equals(valueInMap, defaultValue)) { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java new file mode 100644 index 00000000..3641730d --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/ModelSeed.java | |||
@@ -0,0 +1,86 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.seed; | ||
7 | |||
8 | import tools.refinery.store.map.Cursor; | ||
9 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
10 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
11 | import tools.refinery.store.tuple.Tuple; | ||
12 | |||
13 | import java.util.Collections; | ||
14 | import java.util.LinkedHashMap; | ||
15 | import java.util.Map; | ||
16 | import java.util.function.Consumer; | ||
17 | |||
18 | public class ModelSeed { | ||
19 | private final int nodeCount; | ||
20 | private final Map<AnyPartialSymbol, Seed<?>> seeds; | ||
21 | |||
22 | private ModelSeed(int nodeCount, Map<AnyPartialSymbol, Seed<?>> seeds) { | ||
23 | this.nodeCount = nodeCount; | ||
24 | this.seeds = seeds; | ||
25 | } | ||
26 | |||
27 | public int getNodeCount() { | ||
28 | return nodeCount; | ||
29 | } | ||
30 | |||
31 | public <A> Seed<A> getSeed(PartialSymbol<A, ?> partialSymbol) { | ||
32 | var seed = seeds.get(partialSymbol); | ||
33 | if (seed == null) { | ||
34 | throw new IllegalArgumentException("No seed for partial symbol " + partialSymbol); | ||
35 | } | ||
36 | // The builder makes sure only well-typed seeds can be added. | ||
37 | @SuppressWarnings("unchecked") | ||
38 | var typedSeed = (Seed<A>) seed; | ||
39 | return typedSeed; | ||
40 | } | ||
41 | |||
42 | public <A> Cursor<Tuple, A> getCursor(PartialSymbol<A, ?> partialSymbol, A defaultValue) { | ||
43 | return getSeed(partialSymbol).getCursor(defaultValue, nodeCount); | ||
44 | } | ||
45 | |||
46 | public static Builder builder(int nodeCount) { | ||
47 | return new Builder(nodeCount); | ||
48 | } | ||
49 | |||
50 | public static class Builder { | ||
51 | private final int nodeCount; | ||
52 | private final Map<AnyPartialSymbol, Seed<?>> seeds = new LinkedHashMap<>(); | ||
53 | |||
54 | private Builder(int nodeCount) { | ||
55 | if (nodeCount < 0) { | ||
56 | throw new IllegalArgumentException("Node count must not be negative"); | ||
57 | } | ||
58 | this.nodeCount = nodeCount; | ||
59 | } | ||
60 | |||
61 | public <A> Builder seed(PartialSymbol<A, ?> partialSymbol, Seed<A> seed) { | ||
62 | if (seed.arity() != partialSymbol.arity()) { | ||
63 | throw new IllegalStateException("Expected seed of arity %d for partial symbol %s, but got %d instead" | ||
64 | .formatted(partialSymbol.arity(), partialSymbol, seed.arity())); | ||
65 | } | ||
66 | if (!seed.valueType().equals(partialSymbol.abstractDomain().abstractType())) { | ||
67 | throw new IllegalStateException("Expected seed of type %s for partial symbol %s, but got %s instead" | ||
68 | .formatted(partialSymbol.abstractDomain().abstractType(), partialSymbol, seed.valueType())); | ||
69 | } | ||
70 | if (seeds.put(partialSymbol, seed) != null) { | ||
71 | throw new IllegalArgumentException("Duplicate seed for partial symbol " + partialSymbol); | ||
72 | } | ||
73 | return this; | ||
74 | } | ||
75 | |||
76 | public <A> Builder seed(PartialSymbol<A, ?> partialSymbol, Consumer<Seed.Builder<A>> callback) { | ||
77 | var builder = Seed.builder(partialSymbol); | ||
78 | callback.accept(builder); | ||
79 | return seed(partialSymbol, builder.build()); | ||
80 | } | ||
81 | |||
82 | public ModelSeed build() { | ||
83 | return new ModelSeed(nodeCount, Collections.unmodifiableMap(seeds)); | ||
84 | } | ||
85 | } | ||
86 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java index 64b98683..732efbcc 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java | |||
@@ -42,7 +42,7 @@ public interface Seed<T> { | |||
42 | class Builder<T> { | 42 | class Builder<T> { |
43 | private final int arity; | 43 | private final int arity; |
44 | private final Class<T> valueType; | 44 | private final Class<T> valueType; |
45 | private final T reducedValue; | 45 | private T reducedValue; |
46 | private final Map<Tuple, T> map = new LinkedHashMap<>(); | 46 | private final Map<Tuple, T> map = new LinkedHashMap<>(); |
47 | 47 | ||
48 | private Builder(int arity, Class<T> valueType, T reducedValue) { | 48 | private Builder(int arity, Class<T> valueType, T reducedValue) { |
@@ -51,6 +51,11 @@ public interface Seed<T> { | |||
51 | this.reducedValue = reducedValue; | 51 | this.reducedValue = reducedValue; |
52 | } | 52 | } |
53 | 53 | ||
54 | public Builder<T> reducedValue(T reducedValue) { | ||
55 | this.reducedValue = reducedValue; | ||
56 | return this; | ||
57 | } | ||
58 | |||
54 | public Builder<T> put(Tuple key, T value) { | 59 | public Builder<T> put(Tuple key, T value) { |
55 | if (key.getSize() != arity) { | 60 | if (key.getSize() != arity) { |
56 | throw new IllegalArgumentException("Expected %s to have %d elements".formatted(key, arity)); | 61 | throw new IllegalArgumentException("Expected %s to have %d elements".formatted(key, arity)); |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java index 884d6515..9af457d8 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/SeedInitializer.java | |||
@@ -7,21 +7,22 @@ package tools.refinery.store.reasoning.seed; | |||
7 | 7 | ||
8 | import tools.refinery.store.model.Model; | 8 | import tools.refinery.store.model.Model; |
9 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | 9 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; |
10 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
10 | import tools.refinery.store.representation.Symbol; | 11 | import tools.refinery.store.representation.Symbol; |
11 | 12 | ||
12 | public class SeedInitializer<T> implements PartialModelInitializer { | 13 | public class SeedInitializer<T> implements PartialModelInitializer { |
13 | private final Symbol<T> symbol; | 14 | private final Symbol<T> symbol; |
14 | private final Seed<T> seed; | 15 | private final PartialSymbol<T, ?> partialSymbol; |
15 | 16 | ||
16 | public SeedInitializer(Symbol<T> symbol, Seed<T> seed) { | 17 | public SeedInitializer(Symbol<T> symbol, PartialSymbol<T, ?> partialSymbol) { |
17 | this.symbol = symbol; | 18 | this.symbol = symbol; |
18 | this.seed = seed; | 19 | this.partialSymbol = partialSymbol; |
19 | } | 20 | } |
20 | 21 | ||
21 | @Override | 22 | @Override |
22 | public void initialize(Model model, int nodeCount) { | 23 | public void initialize(Model model, ModelSeed modelSeed) { |
23 | var interpretation = model.getInterpretation(symbol); | 24 | var interpretation = model.getInterpretation(symbol); |
24 | var cursor = seed.getCursor(symbol.defaultValue(), nodeCount); | 25 | var cursor = modelSeed.getCursor(partialSymbol, symbol.defaultValue()); |
25 | interpretation.putAll(cursor); | 26 | interpretation.putAll(cursor); |
26 | } | 27 | } |
27 | } | 28 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java index fe8e8d6c..aee74eb3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java | |||
@@ -32,11 +32,11 @@ import tools.refinery.store.representation.TruthValue; | |||
32 | public final class PartialRelationTranslator extends PartialSymbolTranslator<TruthValue, Boolean> { | 32 | public final class PartialRelationTranslator extends PartialSymbolTranslator<TruthValue, Boolean> { |
33 | private final PartialRelation partialRelation; | 33 | private final PartialRelation partialRelation; |
34 | private PartialRelationRewriter rewriter; | 34 | private PartialRelationRewriter rewriter; |
35 | private Query<Boolean> query; | 35 | private RelationalQuery query; |
36 | private Query<Boolean> may; | 36 | private RelationalQuery may; |
37 | private Query<Boolean> must; | 37 | private RelationalQuery must; |
38 | private Query<Boolean> candidateMay; | 38 | private RelationalQuery candidateMay; |
39 | private Query<Boolean> candidateMust; | 39 | private RelationalQuery candidateMust; |
40 | private RoundingMode roundingMode; | 40 | private RoundingMode roundingMode; |
41 | 41 | ||
42 | private PartialRelationTranslator(PartialRelation partialRelation) { | 42 | private PartialRelationTranslator(PartialRelation partialRelation) { |
@@ -197,20 +197,41 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru | |||
197 | } | 197 | } |
198 | 198 | ||
199 | private void liftQueries(ModelStoreBuilder storeBuilder) { | 199 | private void liftQueries(ModelStoreBuilder storeBuilder) { |
200 | if (query != null) { | 200 | if (rewriter instanceof QueryBasedRelationRewriter queryBasedRelationRewriter) { |
201 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | 201 | liftQueriesFromQueryBasedRewriter(queryBasedRelationRewriter); |
202 | if (may == null) { | 202 | } else if (query != null) { |
203 | may = reasoningBuilder.lift(Modality.MAY, Concreteness.PARTIAL, query); | 203 | liftQueriesFromFourValuedQuery(storeBuilder); |
204 | } | 204 | } |
205 | if (must == null) { | 205 | } |
206 | must = reasoningBuilder.lift(Modality.MUST, Concreteness.PARTIAL, query); | 206 | |
207 | } | 207 | private void liftQueriesFromQueryBasedRewriter(QueryBasedRelationRewriter queryBasedRelationRewriter) { |
208 | if (candidateMay == null) { | 208 | if (may == null) { |
209 | candidateMay = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); | 209 | may = queryBasedRelationRewriter.getMay(); |
210 | } | 210 | } |
211 | if (candidateMust == null) { | 211 | if (must == null) { |
212 | candidateMust = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); | 212 | must = queryBasedRelationRewriter.getMust(); |
213 | } | 213 | } |
214 | if (candidateMay == null) { | ||
215 | candidateMay = queryBasedRelationRewriter.getCandidateMay(); | ||
216 | } | ||
217 | if (candidateMust == null) { | ||
218 | candidateMust = queryBasedRelationRewriter.getCandidateMust(); | ||
219 | } | ||
220 | } | ||
221 | |||
222 | private void liftQueriesFromFourValuedQuery(ModelStoreBuilder storeBuilder) { | ||
223 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | ||
224 | if (may == null) { | ||
225 | may = reasoningBuilder.lift(Modality.MAY, Concreteness.PARTIAL, query); | ||
226 | } | ||
227 | if (must == null) { | ||
228 | must = reasoningBuilder.lift(Modality.MUST, Concreteness.PARTIAL, query); | ||
229 | } | ||
230 | if (candidateMay == null) { | ||
231 | candidateMay = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); | ||
232 | } | ||
233 | if (candidateMust == null) { | ||
234 | candidateMust = reasoningBuilder.lift(Modality.MAY, Concreteness.CANDIDATE, query); | ||
214 | } | 235 | } |
215 | } | 236 | } |
216 | 237 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java index 07d1d19b..542acdb3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialSymbolTranslator.java | |||
@@ -12,7 +12,6 @@ import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | |||
12 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | 12 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; |
13 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | 13 | import tools.refinery.store.reasoning.refinement.StorageRefiner; |
14 | import tools.refinery.store.reasoning.representation.PartialSymbol; | 14 | import tools.refinery.store.reasoning.representation.PartialSymbol; |
15 | import tools.refinery.store.reasoning.seed.Seed; | ||
16 | import tools.refinery.store.reasoning.seed.SeedInitializer; | 15 | import tools.refinery.store.reasoning.seed.SeedInitializer; |
17 | import tools.refinery.store.representation.AnySymbol; | 16 | import tools.refinery.store.representation.AnySymbol; |
18 | import tools.refinery.store.representation.Symbol; | 17 | import tools.refinery.store.representation.Symbol; |
@@ -100,20 +99,6 @@ public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartial | |||
100 | return this; | 99 | return this; |
101 | } | 100 | } |
102 | 101 | ||
103 | public <T> PartialSymbolTranslator<A, C> seed(Seed<T> seed) { | ||
104 | if (storageSymbol == null) { | ||
105 | throw new IllegalArgumentException("Seed requires setting a storage symbol"); | ||
106 | } | ||
107 | if (!seed.valueType().equals(storageSymbol.valueType())) { | ||
108 | throw new IllegalArgumentException("Seed type %s does not match storage symbol type %s" | ||
109 | .formatted(seed.valueType(), storageSymbol.valueType())); | ||
110 | } | ||
111 | // The guard clause only allows a well-typed seed. | ||
112 | @SuppressWarnings("unchecked") | ||
113 | var typedStorageSymbol = (Symbol<T>) storageSymbol; | ||
114 | return initializer(new SeedInitializer<>(typedStorageSymbol, seed)); | ||
115 | } | ||
116 | |||
117 | @Override | 102 | @Override |
118 | public void configure(ModelStoreBuilder storeBuilder) { | 103 | public void configure(ModelStoreBuilder storeBuilder) { |
119 | checkNotConfigured(); | 104 | checkNotConfigured(); |
@@ -132,6 +117,7 @@ public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartial | |||
132 | registerStorageRefiner(reasoningBuilder, storageRefiner); | 117 | registerStorageRefiner(reasoningBuilder, storageRefiner); |
133 | } | 118 | } |
134 | } | 119 | } |
120 | createFallbackInitializer(); | ||
135 | if (initializer != null) { | 121 | if (initializer != null) { |
136 | reasoningBuilder.initializer(initializer); | 122 | reasoningBuilder.initializer(initializer); |
137 | } | 123 | } |
@@ -144,6 +130,17 @@ public abstract sealed class PartialSymbolTranslator<A, C> implements AnyPartial | |||
144 | reasoningBuilder.storageRefiner(typedStorageSymbol, factory); | 130 | reasoningBuilder.storageRefiner(typedStorageSymbol, factory); |
145 | } | 131 | } |
146 | 132 | ||
133 | private void createFallbackInitializer() { | ||
134 | if (initializer == null && | ||
135 | storageSymbol != null && | ||
136 | storageSymbol.valueType().equals(partialSymbol.abstractDomain().abstractType())) { | ||
137 | // The guard clause makes this safe. | ||
138 | @SuppressWarnings("unchecked") | ||
139 | var typedStorageSymbol = (Symbol<A>) storageSymbol; | ||
140 | initializer = new SeedInitializer<>(typedStorageSymbol, partialSymbol); | ||
141 | } | ||
142 | } | ||
143 | |||
147 | public PartialInterpretation.Factory<A, C> getInterpretationFactory() { | 144 | public PartialInterpretation.Factory<A, C> getInterpretationFactory() { |
148 | checkConfigured(); | 145 | checkConfigured(); |
149 | return interpretationFactory; | 146 | return interpretationFactory; |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java new file mode 100644 index 00000000..d8db4ec4 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRefiner.java | |||
@@ -0,0 +1,64 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; | ||
11 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
12 | import tools.refinery.store.representation.Symbol; | ||
13 | import tools.refinery.store.representation.TruthValue; | ||
14 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
15 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
16 | import tools.refinery.store.tuple.Tuple; | ||
17 | |||
18 | public class EqualsRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> { | ||
19 | private final Interpretation<CardinalityInterval> countInterpretation; | ||
20 | |||
21 | private EqualsRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol, | ||
22 | Symbol<CardinalityInterval> countSymbol) { | ||
23 | super(adapter, partialSymbol); | ||
24 | countInterpretation = adapter.getModel().getInterpretation(countSymbol); | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public boolean merge(Tuple key, TruthValue value) { | ||
29 | if (value == TruthValue.UNKNOWN) { | ||
30 | return true; | ||
31 | } | ||
32 | if (value == TruthValue.ERROR) { | ||
33 | return false; | ||
34 | } | ||
35 | int left = key.get(0); | ||
36 | int right = key.get(1); | ||
37 | boolean isDiagonal = left == right; | ||
38 | if (isDiagonal && value == TruthValue.FALSE) { | ||
39 | return false; | ||
40 | } | ||
41 | if (!isDiagonal) { | ||
42 | return !value.may(); | ||
43 | } | ||
44 | if (value != TruthValue.TRUE) { | ||
45 | throw new IllegalArgumentException("Unknown TruthValue: " + value); | ||
46 | } | ||
47 | // {@code isDiagonal} is true, so this could be {@code left} or {@code right}. | ||
48 | var unaryKey = Tuple.of(left); | ||
49 | var currentCount = countInterpretation.get(unaryKey); | ||
50 | if (currentCount == null) { | ||
51 | return false; | ||
52 | } | ||
53 | var newCount = currentCount.meet(CardinalityIntervals.LONE); | ||
54 | if (newCount.isEmpty()) { | ||
55 | return false; | ||
56 | } | ||
57 | countInterpretation.put(unaryKey, newCount); | ||
58 | return true; | ||
59 | } | ||
60 | |||
61 | public static Factory<TruthValue, Boolean> of(Symbol<CardinalityInterval> countSymbol) { | ||
62 | return (adapter, partialSymbol) -> new EqualsRefiner(adapter, partialSymbol, countSymbol); | ||
63 | } | ||
64 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java new file mode 100644 index 00000000..c7bc9fff --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java | |||
@@ -0,0 +1,84 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.query.dnf.Query; | ||
9 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
10 | import tools.refinery.store.query.literal.AbstractCallLiteral; | ||
11 | import tools.refinery.store.query.literal.CallLiteral; | ||
12 | import tools.refinery.store.query.literal.Literal; | ||
13 | import tools.refinery.store.query.term.Variable; | ||
14 | import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter; | ||
15 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
16 | import tools.refinery.store.reasoning.literal.Modality; | ||
17 | import tools.refinery.store.representation.cardinality.UpperCardinalities; | ||
18 | import tools.refinery.store.representation.cardinality.UpperCardinality; | ||
19 | |||
20 | import java.util.List; | ||
21 | import java.util.Set; | ||
22 | |||
23 | import static tools.refinery.store.query.literal.Literals.check; | ||
24 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.constant; | ||
25 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.lessEq; | ||
26 | |||
27 | class EqualsRelationRewriter extends QueryBasedRelationRewriter { | ||
28 | private EqualsRelationRewriter(RelationalQuery may, RelationalQuery must) { | ||
29 | super(may, must, may, may); | ||
30 | } | ||
31 | |||
32 | @Override | ||
33 | public List<Literal> rewriteLiteral(Set<Variable> positiveVariables, AbstractCallLiteral literal, | ||
34 | Modality modality, Concreteness concreteness) { | ||
35 | if (!(literal instanceof CallLiteral callLiteral)) { | ||
36 | return super.rewriteLiteral(positiveVariables, literal, modality, concreteness); | ||
37 | } | ||
38 | var left = callLiteral.getArguments().get(0).asNodeVariable(); | ||
39 | var right = callLiteral.getArguments().get(1).asNodeVariable(); | ||
40 | boolean useMay = modality == Modality.MAY || concreteness == Concreteness.CANDIDATE; | ||
41 | return switch (callLiteral.getPolarity()) { | ||
42 | case POSITIVE, TRANSITIVE -> { | ||
43 | if (useMay) { | ||
44 | if (positiveVariables.contains(left) || positiveVariables.contains(right)) { | ||
45 | // No need to enumerate arguments if at least one is already bound, since they will be unified. | ||
46 | yield List.of(left.isEquivalent(right)); | ||
47 | } else { | ||
48 | yield List.of( | ||
49 | left.isEquivalent(right), | ||
50 | getMay().call(left, right) | ||
51 | ); | ||
52 | } | ||
53 | } else { | ||
54 | yield List.of( | ||
55 | left.isEquivalent(right), | ||
56 | getMust().call(left, right) | ||
57 | ); | ||
58 | } | ||
59 | } | ||
60 | case NEGATIVE -> { | ||
61 | if (useMay) { | ||
62 | yield List.of(left.notEquivalent(right)); | ||
63 | } else { | ||
64 | yield super.rewriteLiteral(positiveVariables, literal, modality, concreteness); | ||
65 | } | ||
66 | } | ||
67 | }; | ||
68 | } | ||
69 | |||
70 | public static EqualsRelationRewriter of(UpperCardinalityView upperCardinalityView) { | ||
71 | var may = Query.of("MAY_EQUALS", (builder, p1, p2) -> builder | ||
72 | .clause( | ||
73 | p1.isEquivalent(p2), | ||
74 | upperCardinalityView.call(p1, Variable.of(UpperCardinality.class)) | ||
75 | )); | ||
76 | var must = Query.of("MUST_EQUALS", (builder, p1, p2) -> builder | ||
77 | .clause(UpperCardinality.class, upper -> List.of( | ||
78 | p1.isEquivalent(p2), | ||
79 | upperCardinalityView.call(p1, upper), | ||
80 | check(lessEq(upper, constant(UpperCardinalities.ONE))) | ||
81 | ))); | ||
82 | return new EqualsRelationRewriter(may, must); | ||
83 | } | ||
84 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java new file mode 100644 index 00000000..f134fe92 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/ExistsRefiner.java | |||
@@ -0,0 +1,55 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; | ||
11 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
12 | import tools.refinery.store.representation.Symbol; | ||
13 | import tools.refinery.store.representation.TruthValue; | ||
14 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
15 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
16 | import tools.refinery.store.tuple.Tuple; | ||
17 | |||
18 | public class ExistsRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> { | ||
19 | private final Interpretation<CardinalityInterval> countInterpretation; | ||
20 | |||
21 | private ExistsRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol, | ||
22 | Symbol<CardinalityInterval> countSymbol) { | ||
23 | super(adapter, partialSymbol); | ||
24 | countInterpretation = adapter.getModel().getInterpretation(countSymbol); | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public boolean merge(Tuple key, TruthValue value) { | ||
29 | var currentCount = countInterpretation.get(key); | ||
30 | if (currentCount == null) { | ||
31 | return false; | ||
32 | } | ||
33 | CardinalityInterval newCount; | ||
34 | switch (value) { | ||
35 | case UNKNOWN -> { | ||
36 | return true; | ||
37 | } | ||
38 | case TRUE -> newCount = currentCount.meet(CardinalityIntervals.SOME); | ||
39 | case FALSE -> newCount = currentCount.meet(CardinalityIntervals.NONE); | ||
40 | case ERROR -> { | ||
41 | return false; | ||
42 | } | ||
43 | default -> throw new IllegalArgumentException("Unknown TruthValue: " + value); | ||
44 | } | ||
45 | if (newCount.isEmpty()) { | ||
46 | return false; | ||
47 | } | ||
48 | countInterpretation.put(key, newCount); | ||
49 | return true; | ||
50 | } | ||
51 | |||
52 | public static Factory<TruthValue, Boolean> of(Symbol<CardinalityInterval> countSymbol) { | ||
53 | return (adapter, partialSymbol) -> new ExistsRefiner(adapter, partialSymbol, countSymbol); | ||
54 | } | ||
55 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/LowerCardinalityView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/LowerCardinalityView.java new file mode 100644 index 00000000..9873888c --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/LowerCardinalityView.java | |||
@@ -0,0 +1,22 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.query.term.Parameter; | ||
9 | import tools.refinery.store.query.view.AbstractFunctionView; | ||
10 | import tools.refinery.store.representation.Symbol; | ||
11 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
12 | |||
13 | class LowerCardinalityView extends AbstractFunctionView<CardinalityInterval> { | ||
14 | public LowerCardinalityView(Symbol<CardinalityInterval> symbol) { | ||
15 | super(symbol, "lower", new Parameter(Integer.class)); | ||
16 | } | ||
17 | |||
18 | @Override | ||
19 | protected Object forwardMapValue(CardinalityInterval value) { | ||
20 | return value.lowerBound(); | ||
21 | } | ||
22 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java new file mode 100644 index 00000000..6917b8ed --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectInitializer.java | |||
@@ -0,0 +1,93 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | ||
11 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
12 | import tools.refinery.store.representation.Symbol; | ||
13 | import tools.refinery.store.representation.TruthValue; | ||
14 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
15 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
16 | import tools.refinery.store.tuple.Tuple; | ||
17 | |||
18 | import java.util.Arrays; | ||
19 | |||
20 | class MultiObjectInitializer implements PartialModelInitializer { | ||
21 | private final Symbol<CardinalityInterval> countSymbol; | ||
22 | |||
23 | public MultiObjectInitializer(Symbol<CardinalityInterval> countSymbol) { | ||
24 | this.countSymbol = countSymbol; | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public void initialize(Model model, ModelSeed modelSeed) { | ||
29 | var intervals = new CardinalityInterval[modelSeed.getNodeCount()]; | ||
30 | Arrays.fill(intervals, CardinalityIntervals.SET); | ||
31 | initializeExists(intervals, modelSeed); | ||
32 | initializeEquals(intervals, modelSeed); | ||
33 | var countInterpretation = model.getInterpretation(countSymbol); | ||
34 | for (int i = 0; i < intervals.length; i++) { | ||
35 | var interval = intervals[i]; | ||
36 | if (interval.isEmpty()) { | ||
37 | throw new IllegalArgumentException("Inconsistent existence or equality for node " + i); | ||
38 | } | ||
39 | countInterpretation.put(Tuple.of(i), intervals[i]); | ||
40 | } | ||
41 | } | ||
42 | |||
43 | private void initializeExists(CardinalityInterval[] intervals, ModelSeed modelSeed) { | ||
44 | var cursor = modelSeed.getCursor(ReasoningAdapter.EXISTS_SYMBOL, TruthValue.UNKNOWN); | ||
45 | while (cursor.move()) { | ||
46 | int i = cursor.getKey().get(0); | ||
47 | checkNodeId(intervals, i); | ||
48 | switch (cursor.getValue()) { | ||
49 | case TRUE -> intervals[i] = intervals[i].meet(CardinalityIntervals.SOME); | ||
50 | case FALSE -> intervals[i] = intervals[i].meet(CardinalityIntervals.NONE); | ||
51 | case ERROR -> throw new IllegalArgumentException("Inconsistent existence for node " + i); | ||
52 | default -> throw new IllegalArgumentException("Invalid existence truth value %s for node %d" | ||
53 | .formatted(cursor.getValue(), i)); | ||
54 | } | ||
55 | } | ||
56 | } | ||
57 | |||
58 | private void initializeEquals(CardinalityInterval[] intervals, ModelSeed modelSeed) { | ||
59 | var seed = modelSeed.getSeed(ReasoningAdapter.EQUALS_SYMBOL); | ||
60 | var cursor = seed.getCursor(TruthValue.FALSE, modelSeed.getNodeCount()); | ||
61 | while (cursor.move()) { | ||
62 | var key = cursor.getKey(); | ||
63 | int i = key.get(0); | ||
64 | int otherIndex = key.get(1); | ||
65 | if (i != otherIndex) { | ||
66 | throw new IllegalArgumentException("Off-diagonal equivalence (%d, %d) is not permitted" | ||
67 | .formatted(i, otherIndex)); | ||
68 | } | ||
69 | checkNodeId(intervals, i); | ||
70 | switch (cursor.getValue()) { | ||
71 | case TRUE -> intervals[i] = intervals[i].meet(CardinalityIntervals.LONE); | ||
72 | case UNKNOWN -> { | ||
73 | // Nothing do to, {@code intervals} is initialized with unknown equality. | ||
74 | } | ||
75 | case ERROR -> throw new IllegalArgumentException("Inconsistent equality for node " + i); | ||
76 | default -> throw new IllegalArgumentException("Invalid equality truth value %s for node %d" | ||
77 | .formatted(cursor.getValue(), i)); | ||
78 | } | ||
79 | } | ||
80 | for (int i = 0; i < intervals.length; i++) { | ||
81 | if (seed.get(Tuple.of(i, i)) == TruthValue.FALSE) { | ||
82 | throw new IllegalArgumentException("Inconsistent equality for node " + i); | ||
83 | } | ||
84 | } | ||
85 | } | ||
86 | |||
87 | private void checkNodeId(CardinalityInterval[] intervals, int nodeId) { | ||
88 | if (nodeId < 0 || nodeId >= intervals.length) { | ||
89 | throw new IllegalArgumentException("Expected node id %d to be lower than model size %d" | ||
90 | .formatted(nodeId, intervals.length)); | ||
91 | } | ||
92 | } | ||
93 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java new file mode 100644 index 00000000..e48934d8 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectStorageRefiner.java | |||
@@ -0,0 +1,45 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | import tools.refinery.store.model.Model; | ||
10 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | ||
11 | import tools.refinery.store.representation.Symbol; | ||
12 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
13 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
14 | import tools.refinery.store.tuple.Tuple; | ||
15 | |||
16 | class MultiObjectStorageRefiner implements StorageRefiner { | ||
17 | private final Interpretation<CardinalityInterval> countInterpretation; | ||
18 | |||
19 | public MultiObjectStorageRefiner(Symbol<CardinalityInterval> countSymbol, Model model) { | ||
20 | countInterpretation = model.getInterpretation(countSymbol); | ||
21 | } | ||
22 | |||
23 | @Override | ||
24 | public boolean split(int parentNode, int childNode) { | ||
25 | var parentKey = Tuple.of(parentNode); | ||
26 | var parentCount = countInterpretation.get(parentKey); | ||
27 | if (parentCount == null) { | ||
28 | return false; | ||
29 | } | ||
30 | var newParentCount = parentCount.take(1); | ||
31 | if (newParentCount.isEmpty()) { | ||
32 | return false; | ||
33 | } | ||
34 | var childKey = Tuple.of(childNode); | ||
35 | countInterpretation.put(parentKey, newParentCount); | ||
36 | countInterpretation.put(childKey, CardinalityIntervals.ONE); | ||
37 | return true; | ||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public boolean cleanup(int nodeToDelete) { | ||
42 | var previousCount = countInterpretation.put(Tuple.of(nodeToDelete), null); | ||
43 | return previousCount.lowerBound() == 0; | ||
44 | } | ||
45 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java new file mode 100644 index 00000000..0367214b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java | |||
@@ -0,0 +1,60 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.model.ModelStoreBuilder; | ||
9 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
10 | import tools.refinery.store.query.dnf.Query; | ||
11 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
12 | import tools.refinery.store.reasoning.ReasoningBuilder; | ||
13 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
14 | import tools.refinery.store.reasoning.translator.RoundingMode; | ||
15 | import tools.refinery.store.representation.Symbol; | ||
16 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
17 | import tools.refinery.store.representation.cardinality.UpperCardinalities; | ||
18 | import tools.refinery.store.representation.cardinality.UpperCardinality; | ||
19 | |||
20 | import java.util.List; | ||
21 | |||
22 | import static tools.refinery.store.query.literal.Literals.check; | ||
23 | import static tools.refinery.store.query.term.int_.IntTerms.constant; | ||
24 | import static tools.refinery.store.query.term.int_.IntTerms.greaterEq; | ||
25 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.constant; | ||
26 | import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.greaterEq; | ||
27 | |||
28 | public class MultiObjectTranslator implements ModelStoreConfiguration { | ||
29 | private final Symbol<CardinalityInterval> countSymbol = Symbol.of("COUNT", 1, CardinalityInterval.class, | ||
30 | null); | ||
31 | private final LowerCardinalityView lowerCardinalityView = new LowerCardinalityView(countSymbol); | ||
32 | private final UpperCardinalityView upperCardinalityView = new UpperCardinalityView(countSymbol); | ||
33 | |||
34 | @Override | ||
35 | public void apply(ModelStoreBuilder storeBuilder) { | ||
36 | storeBuilder.symbol(countSymbol); | ||
37 | |||
38 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL) | ||
39 | .may(Query.of("MAY_EXISTS", (builder, p1) -> builder | ||
40 | .clause(UpperCardinality.class, upper -> List.of( | ||
41 | upperCardinalityView.call(p1, upper), | ||
42 | check(greaterEq(upper, constant(UpperCardinalities.ONE))) | ||
43 | )))) | ||
44 | .must(Query.of("MUST_EXISTS", (builder, p1) -> builder | ||
45 | .clause(Integer.class, lower -> List.of( | ||
46 | lowerCardinalityView.call(p1, lower), | ||
47 | check(greaterEq(lower, constant(1))) | ||
48 | )))) | ||
49 | .roundingMode(RoundingMode.PREFER_FALSE) | ||
50 | .refiner(ExistsRefiner.of(countSymbol))); | ||
51 | |||
52 | storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EQUALS_SYMBOL) | ||
53 | .rewriter(EqualsRelationRewriter.of(upperCardinalityView)) | ||
54 | .refiner(EqualsRefiner.of(countSymbol))); | ||
55 | |||
56 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | ||
57 | reasoningBuilder.initializer(new MultiObjectInitializer(countSymbol)); | ||
58 | reasoningBuilder.storageRefiner(countSymbol, MultiObjectStorageRefiner::new); | ||
59 | } | ||
60 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/UpperCardinalityView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/UpperCardinalityView.java new file mode 100644 index 00000000..6be6ae1b --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/UpperCardinalityView.java | |||
@@ -0,0 +1,23 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.store.query.term.Parameter; | ||
9 | import tools.refinery.store.query.view.AbstractFunctionView; | ||
10 | import tools.refinery.store.representation.Symbol; | ||
11 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
12 | import tools.refinery.store.representation.cardinality.UpperCardinality; | ||
13 | |||
14 | class UpperCardinalityView extends AbstractFunctionView<CardinalityInterval> { | ||
15 | public UpperCardinalityView(Symbol<CardinalityInterval> symbol) { | ||
16 | super(symbol, "upper", new Parameter(UpperCardinality.class)); | ||
17 | } | ||
18 | |||
19 | @Override | ||
20 | protected Object forwardMapValue(CardinalityInterval value) { | ||
21 | return value.upperBound(); | ||
22 | } | ||
23 | } | ||