diff options
author | Kristóf Marussy <kristof@marussy.com> | 2024-07-02 20:08:33 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2024-07-02 20:44:48 +0200 |
commit | d5b54f9b3f07bf6b2e044ad0b35176c4f428077e (patch) | |
tree | 87b5423ade2a8ca82402ddd4df925c75deaa7e2f /subprojects | |
parent | fix(semantics): traceability for internal rules (diff) | |
download | refinery-d5b54f9b3f07bf6b2e044ad0b35176c4f428077e.tar.gz refinery-d5b54f9b3f07bf6b2e044ad0b35176c4f428077e.tar.zst refinery-d5b54f9b3f07bf6b2e044ad0b35176c4f428077e.zip |
fix(reasoning): do not propagate invalidated objects
Diffstat (limited to 'subprojects')
5 files changed, 88 insertions, 28 deletions
diff --git a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java index efe1464e..d564ff66 100644 --- a/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java +++ b/subprojects/logic/src/main/java/tools/refinery/logic/term/cardinalityinterval/NonEmptyCardinalityInterval.java | |||
@@ -32,8 +32,7 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper | |||
32 | 32 | ||
33 | @Override | 33 | @Override |
34 | public boolean isConcrete() { | 34 | public boolean isConcrete() { |
35 | return upperBound instanceof FiniteUpperCardinality finiteUpperCardinality && | 35 | return upperBound instanceof FiniteUpperCardinality(var finiteUpperBound) && finiteUpperBound == lowerBound; |
36 | finiteUpperCardinality.finiteUpperBound() == lowerBound; | ||
37 | } | 36 | } |
38 | 37 | ||
39 | @Override | 38 | @Override |
@@ -49,10 +48,10 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper | |||
49 | 48 | ||
50 | @Override | 49 | @Override |
51 | public boolean isRefinementOf(CardinalityInterval other) { | 50 | public boolean isRefinementOf(CardinalityInterval other) { |
52 | if (!(other instanceof NonEmptyCardinalityInterval nonEmptyOther)) { | 51 | if (!(other instanceof NonEmptyCardinalityInterval(var otherLowerBound, var otherUpperBound))) { |
53 | return false; | 52 | return false; |
54 | } | 53 | } |
55 | return lowerBound >= nonEmptyOther.lowerBound() && upperBound.compareTo(nonEmptyOther.upperBound()) <= 0; | 54 | return lowerBound >= otherLowerBound && upperBound.compareTo(otherUpperBound) <= 0; |
56 | } | 55 | } |
57 | 56 | ||
58 | @Override | 57 | @Override |
@@ -98,9 +97,9 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper | |||
98 | private CardinalityInterval lift(CardinalityInterval other, IntBinaryOperator lowerOperator, | 97 | private CardinalityInterval lift(CardinalityInterval other, IntBinaryOperator lowerOperator, |
99 | BinaryOperator<UpperCardinality> upperOperator, | 98 | BinaryOperator<UpperCardinality> upperOperator, |
100 | CardinalityInterval whenEmpty) { | 99 | CardinalityInterval whenEmpty) { |
101 | if (other instanceof NonEmptyCardinalityInterval nonEmptyOther) { | 100 | if (other instanceof NonEmptyCardinalityInterval(var otherLowerBound, var otherUpperBound)) { |
102 | return CardinalityIntervals.between(lowerOperator.applyAsInt(lowerBound, nonEmptyOther.lowerBound), | 101 | return CardinalityIntervals.between(lowerOperator.applyAsInt(lowerBound, otherLowerBound), |
103 | upperOperator.apply(upperBound, nonEmptyOther.upperBound)); | 102 | upperOperator.apply(upperBound, otherUpperBound)); |
104 | } | 103 | } |
105 | if (other instanceof EmptyCardinalityInterval) { | 104 | if (other instanceof EmptyCardinalityInterval) { |
106 | return whenEmpty; | 105 | return whenEmpty; |
@@ -115,8 +114,8 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper | |||
115 | 114 | ||
116 | @Override | 115 | @Override |
117 | public String toString() { | 116 | public String toString() { |
118 | if (upperBound instanceof FiniteUpperCardinality finiteUpperCardinality && | 117 | if (upperBound instanceof FiniteUpperCardinality(var finiteUpperBound) && |
119 | finiteUpperCardinality.finiteUpperBound() == lowerBound) { | 118 | finiteUpperBound == lowerBound) { |
120 | return "[%d]".formatted(lowerBound); | 119 | return "[%d]".formatted(lowerBound); |
121 | } | 120 | } |
122 | return "[%d..%s]".formatted(lowerBound, upperBound); | 121 | return "[%d..%s]".formatted(lowerBound, upperBound); |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java index e8e6880a..18f238d7 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java | |||
@@ -36,8 +36,4 @@ public final class PartialActionLiterals { | |||
36 | public static FocusActionLiteral focus(NodeVariable parent, NodeVariable child) { | 36 | public static FocusActionLiteral focus(NodeVariable parent, NodeVariable child) { |
37 | return new FocusActionLiteral(parent, child); | 37 | return new FocusActionLiteral(parent, child); |
38 | } | 38 | } |
39 | |||
40 | public static CleanupActionLiteral cleanup(NodeVariable node) { | ||
41 | return new CleanupActionLiteral(node); | ||
42 | } | ||
43 | } | 39 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java index be9fcb9d..41d185d7 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java | |||
@@ -30,10 +30,10 @@ import static tools.refinery.logic.literal.Literals.check; | |||
30 | import static tools.refinery.logic.literal.Literals.not; | 30 | import static tools.refinery.logic.literal.Literals.not; |
31 | import static tools.refinery.logic.term.int_.IntTerms.constant; | 31 | import static tools.refinery.logic.term.int_.IntTerms.constant; |
32 | import static tools.refinery.logic.term.int_.IntTerms.less; | 32 | import static tools.refinery.logic.term.int_.IntTerms.less; |
33 | import static tools.refinery.store.reasoning.ReasoningAdapter.EQUALS_SYMBOL; | ||
33 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add; | 34 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add; |
34 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.remove; | 35 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.remove; |
35 | import static tools.refinery.store.reasoning.literal.PartialLiterals.*; | 36 | import static tools.refinery.store.reasoning.literal.PartialLiterals.*; |
36 | import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; | ||
37 | 37 | ||
38 | public class CrossReferenceUtils { | 38 | public class CrossReferenceUtils { |
39 | private CrossReferenceUtils() { | 39 | private CrossReferenceUtils() { |
@@ -93,7 +93,6 @@ public class CrossReferenceUtils { | |||
93 | var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound); | 93 | var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound); |
94 | propagationBuilder.rule(Rule.of(name + "#lowerSource", (builder, p1, p2) -> builder | 94 | propagationBuilder.rule(Rule.of(name + "#lowerSource", (builder, p1, p2) -> builder |
95 | .clause(UpperCardinality.class, upperBound -> List.of( | 95 | .clause(UpperCardinality.class, upperBound -> List.of( |
96 | not(MULTI_VIEW.call(p1)), | ||
97 | must(sourceType.call(p1)), | 96 | must(sourceType.call(p1)), |
98 | new CountUpperBoundLiteral(upperBound, linkType, List.of(p1, Variable.of())), | 97 | new CountUpperBoundLiteral(upperBound, linkType, List.of(p1, Variable.of())), |
99 | check(UpperCardinalityTerms.lessEq(upperBound, | 98 | check(UpperCardinalityTerms.lessEq(upperBound, |
@@ -127,7 +126,6 @@ public class CrossReferenceUtils { | |||
127 | var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound); | 126 | var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound); |
128 | propagationBuilder.rule(Rule.of(name + "#lowerTarget", (builder, p1, p2) -> builder | 127 | propagationBuilder.rule(Rule.of(name + "#lowerTarget", (builder, p1, p2) -> builder |
129 | .clause(UpperCardinality.class, upperBound -> List.of( | 128 | .clause(UpperCardinality.class, upperBound -> List.of( |
130 | not(MULTI_VIEW.call(p2)), | ||
131 | must(targetType.call(p2)), | 129 | must(targetType.call(p2)), |
132 | new CountUpperBoundLiteral(upperBound, linkType, List.of(Variable.of(), p2)), | 130 | new CountUpperBoundLiteral(upperBound, linkType, List.of(Variable.of(), p2)), |
133 | check(UpperCardinalityTerms.lessEq(upperBound, | 131 | check(UpperCardinalityTerms.lessEq(upperBound, |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java new file mode 100644 index 00000000..f14b4783 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java | |||
@@ -0,0 +1,78 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2024 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.logic.dnf.Query; | ||
9 | import tools.refinery.logic.dnf.RelationalQuery; | ||
10 | import tools.refinery.logic.term.uppercardinality.UpperCardinalities; | ||
11 | import tools.refinery.logic.term.uppercardinality.UpperCardinality; | ||
12 | import tools.refinery.logic.term.uppercardinality.UpperCardinalityTerms; | ||
13 | import tools.refinery.store.dse.propagation.BoundPropagator; | ||
14 | import tools.refinery.store.dse.propagation.PropagationResult; | ||
15 | import tools.refinery.store.dse.propagation.Propagator; | ||
16 | import tools.refinery.store.model.Model; | ||
17 | import tools.refinery.store.model.ModelStoreBuilder; | ||
18 | import tools.refinery.store.query.ModelQueryAdapter; | ||
19 | import tools.refinery.store.query.ModelQueryBuilder; | ||
20 | import tools.refinery.store.query.resultset.ResultSet; | ||
21 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
22 | |||
23 | import java.util.List; | ||
24 | |||
25 | import static tools.refinery.logic.literal.Literals.check; | ||
26 | import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.UPPER_CARDINALITY_VIEW; | ||
27 | |||
28 | /** | ||
29 | * Clean up non-existing objects in a separate propagator to avoid interference with propagation rules that assume | ||
30 | * that each object in their activation set is still part of the model when they are called. | ||
31 | */ | ||
32 | public class CleanupPropagator implements Propagator { | ||
33 | private static final RelationalQuery CLEANUP_QUERY = Query.of("exists#cleanup", (builder, node) -> builder | ||
34 | .clause(UpperCardinality.class, upper -> List.of( | ||
35 | UPPER_CARDINALITY_VIEW.call(node, upper), | ||
36 | check(UpperCardinalityTerms.less(upper, | ||
37 | UpperCardinalityTerms.constant(UpperCardinalities.ONE))) | ||
38 | )) | ||
39 | ); | ||
40 | |||
41 | @Override | ||
42 | public void configure(ModelStoreBuilder storeBuilder) { | ||
43 | storeBuilder.getAdapter(ModelQueryBuilder.class).query(CLEANUP_QUERY); | ||
44 | } | ||
45 | |||
46 | @Override | ||
47 | public BoundPropagator bindToModel(Model model) { | ||
48 | return new BoundCleanupPropagator(model); | ||
49 | } | ||
50 | |||
51 | private static class BoundCleanupPropagator implements BoundPropagator { | ||
52 | private final Model model; | ||
53 | private final ModelQueryAdapter queryEngine; | ||
54 | private final ResultSet<Boolean> resultSet; | ||
55 | private ReasoningAdapter reasoningAdapter; | ||
56 | |||
57 | public BoundCleanupPropagator(Model model) { | ||
58 | this.model = model; | ||
59 | queryEngine = model.getAdapter(ModelQueryAdapter.class); | ||
60 | resultSet = queryEngine.getResultSet(CLEANUP_QUERY); | ||
61 | } | ||
62 | |||
63 | @Override | ||
64 | public PropagationResult propagateOne() { | ||
65 | if (reasoningAdapter == null) { | ||
66 | reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
67 | } | ||
68 | queryEngine.flushChanges(); | ||
69 | boolean propagated = false; | ||
70 | var cursor = resultSet.getAll(); | ||
71 | while (cursor.move()) { | ||
72 | propagated = true; | ||
73 | reasoningAdapter.cleanup(cursor.getKey().get(0)); | ||
74 | } | ||
75 | return propagated ? PropagationResult.PROPAGATED : PropagationResult.UNCHANGED; | ||
76 | } | ||
77 | } | ||
78 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java index be15b6d7..05d96689 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java | |||
@@ -15,7 +15,6 @@ import tools.refinery.logic.term.uppercardinality.UpperCardinalities; | |||
15 | import tools.refinery.logic.term.uppercardinality.UpperCardinality; | 15 | import tools.refinery.logic.term.uppercardinality.UpperCardinality; |
16 | import tools.refinery.logic.term.uppercardinality.UpperCardinalityTerms; | 16 | import tools.refinery.logic.term.uppercardinality.UpperCardinalityTerms; |
17 | import tools.refinery.store.dse.propagation.PropagationBuilder; | 17 | import tools.refinery.store.dse.propagation.PropagationBuilder; |
18 | import tools.refinery.store.dse.transition.Rule; | ||
19 | import tools.refinery.store.dse.transition.objectives.Criteria; | 18 | import tools.refinery.store.dse.transition.objectives.Criteria; |
20 | import tools.refinery.store.dse.transition.objectives.Objectives; | 19 | import tools.refinery.store.dse.transition.objectives.Objectives; |
21 | import tools.refinery.store.model.ModelStoreBuilder; | 20 | import tools.refinery.store.model.ModelStoreBuilder; |
@@ -23,7 +22,6 @@ import tools.refinery.store.model.ModelStoreConfiguration; | |||
23 | import tools.refinery.store.query.view.AnySymbolView; | 22 | import tools.refinery.store.query.view.AnySymbolView; |
24 | import tools.refinery.store.reasoning.ReasoningAdapter; | 23 | import tools.refinery.store.reasoning.ReasoningAdapter; |
25 | import tools.refinery.store.reasoning.ReasoningBuilder; | 24 | import tools.refinery.store.reasoning.ReasoningBuilder; |
26 | import tools.refinery.store.reasoning.actions.PartialActionLiterals; | ||
27 | import tools.refinery.store.reasoning.representation.PartialFunction; | 25 | import tools.refinery.store.reasoning.representation.PartialFunction; |
28 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | 26 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; |
29 | import tools.refinery.store.reasoning.translator.RoundingMode; | 27 | import tools.refinery.store.reasoning.translator.RoundingMode; |
@@ -93,15 +91,6 @@ public class MultiObjectTranslator implements ModelStoreConfiguration { | |||
93 | reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new); | 91 | reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new); |
94 | 92 | ||
95 | storeBuilder.tryGetAdapter(PropagationBuilder.class) | 93 | storeBuilder.tryGetAdapter(PropagationBuilder.class) |
96 | .ifPresent(propagationBuilder -> propagationBuilder.rule( | 94 | .ifPresent(propagationBuilder -> propagationBuilder.propagator(new CleanupPropagator())); |
97 | Rule.of("exists#cleanup", (builder, node) -> builder | ||
98 | .clause(UpperCardinality.class, upper -> List.of( | ||
99 | UPPER_CARDINALITY_VIEW.call(node, upper), | ||
100 | check(UpperCardinalityTerms.less(upper, | ||
101 | UpperCardinalityTerms.constant(UpperCardinalities.ONE))) | ||
102 | )) | ||
103 | .action( | ||
104 | PartialActionLiterals.cleanup(node) | ||
105 | )))); | ||
106 | } | 95 | } |
107 | } | 96 | } |