fix(reasoning): candidate count literal rewriting

author: Kristóf Marussy <kristof@marussy.com> 2024-06-01 14:47:31 +0200
committer: Kristóf Marussy <kristof@marussy.com> 2024-06-01 20:17:47 +0200
commit: efc6158cd3b971547fc77fb042fa7ab7804434b3 (patch)
tree: 7661b5cd430d1ce8b9c2297054ff4b0514abcbe9
parent: feat: generate multiple solutions (diff)
download: refinery-efc6158cd3b971547fc77fb042fa7ab7804434b3.tar.gz
refinery-efc6158cd3b971547fc77fb042fa7ab7804434b3.tar.zst
refinery-efc6158cd3b971547fc77fb042fa7ab7804434b3.zip
1 files changed, 28 insertions, 36 deletions
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
index dc508a7b..f7e86c44 100644
--- 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
@@ -1,5 +1,5 @@
 /*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/>
 *
 * SPDX-License-Identifier: EPL-2.0
 */
@@ -53,38 +53,30 @@ class PartialClauseRewriter {
                        markAsDone(literal);
                        return;
                }
-                if (callLiteral instanceof CountLowerBoundLiteral countLowerBoundLiteral) {
+                switch (callLiteral) {
-                        rewriteCountLowerBound(countLowerBoundLiteral);
+                case CountLowerBoundLiteral countLowerBoundLiteral -> rewriteCountLowerBound(countLowerBoundLiteral);
-                        return;
+                case CountUpperBoundLiteral countUpperBoundLiteral -> rewriteCountUpperBound(countUpperBoundLiteral);
-                }
+                case CountCandidateLowerBoundLiteral countCandidateLowerBoundLiteral ->
-                if (callLiteral instanceof CountUpperBoundLiteral countUpperBoundLiteral) {
+                                rewriteCountCandidateLowerBound(countCandidateLowerBoundLiteral);
-                        rewriteCountUpperBound(countUpperBoundLiteral);
+                case CountCandidateUpperBoundLiteral countCandidateUpperBoundLiteral ->
-                        return;
+                                rewriteCountCandidateUpperBound(countCandidateUpperBoundLiteral);
-                }
+                default -> {
-                if (callLiteral instanceof CountCandidateLowerBoundLiteral countCandidateLowerBoundLiteral) {
+                        var target = callLiteral.getTarget();
-                        rewriteCountCandidateLowerBound(countCandidateLowerBoundLiteral);
+                        switch (target) {
-                        return;
+                        case Dnf dnf -> rewriteRecursively(callLiteral, dnf);
-                }
+                        case ModalConstraint modalConstraint -> {
-                if (callLiteral instanceof CountCandidateUpperBoundLiteral countCandidateUpperBoundLiteral) {
+                                var modality = modalConstraint.modality();
-                        rewriteCountCandidateUpperBound(countCandidateUpperBoundLiteral);
+                                var concreteness = modalConstraint.concreteness();
-                        return;
+                                var constraint = modalConstraint.constraint();
-                }
+                                switch (constraint) {
-                var target = callLiteral.getTarget();
+                                case Dnf dnf -> rewriteRecursively(callLiteral, modality, concreteness, dnf);
-                if (target instanceof Dnf dnf) {
+                                case PartialRelation partialRelation -> rewrite(callLiteral, modality, concreteness, partialRelation);
-                        rewriteRecursively(callLiteral, dnf);
+                                default -> throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint);
-                } else if (target instanceof ModalConstraint modalConstraint) {
+                                }
-                        var modality = modalConstraint.modality();
-                        var concreteness = modalConstraint.concreteness();
-                        var constraint = modalConstraint.constraint();
-                        if (constraint instanceof Dnf dnf) {
-                                rewriteRecursively(callLiteral, modality, concreteness, dnf);
-                        } else if (constraint instanceof PartialRelation partialRelation) {
-                                rewrite(callLiteral, modality, concreteness, partialRelation);
-                        } else {
-                                throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint);
                        }
-                } else {
+                        default -> markAsDone(literal);
-                        markAsDone(literal);
+                        }
+                }
                }
        }
@@ -111,11 +103,11 @@ class PartialClauseRewriter {
                                .call(CallPolarity.POSITIVE, countResult.rewrittenArguments()));
                switch (variablesToCount.size()) {
                case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one)));
-                case 1 -> literals.add(view.call(variablesToCount.get(0),
+                case 1 -> literals.add(view.call(variablesToCount.getFirst(),
                                outputVariable));
                default -> {
                        var firstCount = Variable.of(type);
-                        literals.add(view.call(variablesToCount.get(0), firstCount));
+                        literals.add(view.call(variablesToCount.getFirst(), firstCount));
                        int length = variablesToCount.size();
                        Term<T> accumulator = firstCount;
                        for (int i = 1; i < length; i++) {
@@ -137,11 +129,11 @@ class PartialClauseRewriter {
        }
        private void rewriteCountCandidateLowerBound(CountCandidateLowerBoundLiteral literal) {
-                rewriteCandidateCount(literal, "lower", Modality.MAY);
+                rewriteCandidateCount(literal, "lower", Modality.MUST);
        }
        private void rewriteCountCandidateUpperBound(CountCandidateUpperBoundLiteral literal) {
-                rewriteCandidateCount(literal, "upper", Modality.MUST);
+                rewriteCandidateCount(literal, "upper", Modality.MAY);
        }
        private void rewriteCandidateCount(AbstractCountLiteral<Integer> literal, String name, Modality modality) {
author	Kristóf Marussy <kristof@marussy.com>	2024-06-01 14:47:31 +0200
committer	Kristóf Marussy <kristof@marussy.com>	2024-06-01 20:17:47 +0200
commit	efc6158cd3b971547fc77fb042fa7ab7804434b3 (patch)
tree	7661b5cd430d1ce8b9c2297054ff4b0514abcbe9
parent	feat: generate multiple solutions (diff)
download	refinery-efc6158cd3b971547fc77fb042fa7ab7804434b3.tar.gz refinery-efc6158cd3b971547fc77fb042fa7ab7804434b3.tar.zst refinery-efc6158cd3b971547fc77fb042fa7ab7804434b3.zip

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 index dc508a7b..f7e86c44 100644 --- 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
@@ -1,5 +1,5 @@
1	/*	1	/*
2	* SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>	2	* SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/>
3	*	3	*
4	* SPDX-License-Identifier: EPL-2.0	4	* SPDX-License-Identifier: EPL-2.0
5	*/	5	*/
@@ -53,38 +53,30 @@ class PartialClauseRewriter {
53	markAsDone(literal);	53	markAsDone(literal);
54	return;	54	return;
55	}	55	}
56	if (callLiteral instanceof CountLowerBoundLiteral countLowerBoundLiteral) {	56	switch (callLiteral) {
57	rewriteCountLowerBound(countLowerBoundLiteral);	57	case CountLowerBoundLiteral countLowerBoundLiteral -> rewriteCountLowerBound(countLowerBoundLiteral);
58	return;	58	case CountUpperBoundLiteral countUpperBoundLiteral -> rewriteCountUpperBound(countUpperBoundLiteral);
59	}	59	case CountCandidateLowerBoundLiteral countCandidateLowerBoundLiteral ->
60	if (callLiteral instanceof CountUpperBoundLiteral countUpperBoundLiteral) {	60	rewriteCountCandidateLowerBound(countCandidateLowerBoundLiteral);
61	rewriteCountUpperBound(countUpperBoundLiteral);	61	case CountCandidateUpperBoundLiteral countCandidateUpperBoundLiteral ->
62	return;	62	rewriteCountCandidateUpperBound(countCandidateUpperBoundLiteral);
63	}	63	default -> {
64	if (callLiteral instanceof CountCandidateLowerBoundLiteral countCandidateLowerBoundLiteral) {	64	var target = callLiteral.getTarget();
65	rewriteCountCandidateLowerBound(countCandidateLowerBoundLiteral);	65	switch (target) {
66	return;	66	case Dnf dnf -> rewriteRecursively(callLiteral, dnf);
67	}	67	case ModalConstraint modalConstraint -> {
68	if (callLiteral instanceof CountCandidateUpperBoundLiteral countCandidateUpperBoundLiteral) {	68	var modality = modalConstraint.modality();
69	rewriteCountCandidateUpperBound(countCandidateUpperBoundLiteral);	69	var concreteness = modalConstraint.concreteness();
70	return;	70	var constraint = modalConstraint.constraint();
71	}	71	switch (constraint) {
72	var target = callLiteral.getTarget();	72	case Dnf dnf -> rewriteRecursively(callLiteral, modality, concreteness, dnf);
73	if (target instanceof Dnf dnf) {	73	case PartialRelation partialRelation -> rewrite(callLiteral, modality, concreteness, partialRelation);
74	rewriteRecursively(callLiteral, dnf);	74	default -> throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint);
75	} else if (target instanceof ModalConstraint modalConstraint) {	75	}
76	var modality = modalConstraint.modality();
77	var concreteness = modalConstraint.concreteness();
78	var constraint = modalConstraint.constraint();
79	if (constraint instanceof Dnf dnf) {
80	rewriteRecursively(callLiteral, modality, concreteness, dnf);
81	} else if (constraint instanceof PartialRelation partialRelation) {
82	rewrite(callLiteral, modality, concreteness, partialRelation);
83	} else {
84	throw new IllegalArgumentException("Cannot interpret modal constraint: " + modalConstraint);
85	}	76	}
86	} else {	77	default -> markAsDone(literal);
87	markAsDone(literal);	78	}
		79	}
88	}	80	}
89	}	81	}
90		82
@@ -111,11 +103,11 @@ class PartialClauseRewriter {
111	.call(CallPolarity.POSITIVE, countResult.rewrittenArguments()));	103	.call(CallPolarity.POSITIVE, countResult.rewrittenArguments()));
112	switch (variablesToCount.size()) {	104	switch (variablesToCount.size()) {
113	case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one)));	105	case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one)));
114	case 1 -> literals.add(view.call(variablesToCount.get(0),	106	case 1 -> literals.add(view.call(variablesToCount.getFirst(),
115	outputVariable));	107	outputVariable));
116	default -> {	108	default -> {
117	var firstCount = Variable.of(type);	109	var firstCount = Variable.of(type);
118	literals.add(view.call(variablesToCount.get(0), firstCount));	110	literals.add(view.call(variablesToCount.getFirst(), firstCount));
119	int length = variablesToCount.size();	111	int length = variablesToCount.size();
120	Term<T> accumulator = firstCount;	112	Term<T> accumulator = firstCount;
121	for (int i = 1; i < length; i++) {	113	for (int i = 1; i < length; i++) {
@@ -137,11 +129,11 @@ class PartialClauseRewriter {
137	}	129	}
138		130
139	private void rewriteCountCandidateLowerBound(CountCandidateLowerBoundLiteral literal) {	131	private void rewriteCountCandidateLowerBound(CountCandidateLowerBoundLiteral literal) {
140	rewriteCandidateCount(literal, "lower", Modality.MAY);	132	rewriteCandidateCount(literal, "lower", Modality.MUST);
141	}	133	}
142		134
143	private void rewriteCountCandidateUpperBound(CountCandidateUpperBoundLiteral literal) {	135	private void rewriteCountCandidateUpperBound(CountCandidateUpperBoundLiteral literal) {
144	rewriteCandidateCount(literal, "upper", Modality.MUST);	136	rewriteCandidateCount(literal, "upper", Modality.MAY);
145	}	137	}
146		138
147	private void rewriteCandidateCount(AbstractCountLiteral<Integer> literal, String name, Modality modality) {	139	private void rewriteCandidateCount(AbstractCountLiteral<Integer> literal, String name, Modality modality) {