diff options
author | 2024-05-20 20:41:06 +0200 | |
---|---|---|
committer | 2024-05-26 17:22:33 +0200 | |
commit | 926da55dedad57f43f0f1cf28cdce1137a48a72d (patch) | |
tree | 0bb5e8ee497165283f23cd94a6fa3608ca09be7e /subprojects/language-semantics/src/main/java/tools | |
parent | feat(language): node constants in rule actions (diff) | |
download | refinery-926da55dedad57f43f0f1cf28cdce1137a48a72d.tar.gz refinery-926da55dedad57f43f0f1cf28cdce1137a48a72d.tar.zst refinery-926da55dedad57f43f0f1cf28cdce1137a48a72d.zip |
fix(semantics): negative quantification in rules
Make sure we appropriate quantify over the existence of objects in negative and
transitive calls in rule preconditions.
Diffstat (limited to 'subprojects/language-semantics/src/main/java/tools')
-rw-r--r-- | subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java | 85 |
1 files changed, 61 insertions, 24 deletions
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java index 02b2f920..6c637e19 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java | |||
@@ -15,10 +15,7 @@ import tools.refinery.language.semantics.internal.MutableSeed; | |||
15 | import tools.refinery.language.utils.BuiltinSymbols; | 15 | import tools.refinery.language.utils.BuiltinSymbols; |
16 | import tools.refinery.language.utils.ProblemUtil; | 16 | import tools.refinery.language.utils.ProblemUtil; |
17 | import tools.refinery.logic.Constraint; | 17 | import tools.refinery.logic.Constraint; |
18 | import tools.refinery.logic.dnf.AbstractQueryBuilder; | 18 | import tools.refinery.logic.dnf.*; |
19 | import tools.refinery.logic.dnf.InvalidClauseException; | ||
20 | import tools.refinery.logic.dnf.Query; | ||
21 | import tools.refinery.logic.dnf.RelationalQuery; | ||
22 | import tools.refinery.logic.literal.*; | 19 | import tools.refinery.logic.literal.*; |
23 | import tools.refinery.logic.term.NodeVariable; | 20 | import tools.refinery.logic.term.NodeVariable; |
24 | import tools.refinery.logic.term.Variable; | 21 | import tools.refinery.logic.term.Variable; |
@@ -689,9 +686,9 @@ public class ModelInitializer { | |||
689 | } | 686 | } |
690 | case Atom atom -> { | 687 | case Atom atom -> { |
691 | var target = getPartialRelation(atom.getRelation()); | 688 | var target = getPartialRelation(atom.getRelation()); |
692 | var polarity = atom.isTransitiveClosure() ? CallPolarity.TRANSITIVE : CallPolarity.POSITIVE; | 689 | var constraint = atom.isTransitiveClosure() ? getTransitiveWrapper(target) : target; |
693 | var argumentList = toArgumentList(atom.getArguments(), localScope, literals); | 690 | var argumentList = toArgumentList(atom.getArguments(), localScope, literals); |
694 | literals.add(extractedOuter.modality.wrapConstraint(target).call(polarity, argumentList)); | 691 | literals.add(extractedOuter.modality.wrapConstraint(constraint).call(CallPolarity.POSITIVE, argumentList)); |
695 | } | 692 | } |
696 | case NegationExpr negationExpr -> { | 693 | case NegationExpr negationExpr -> { |
697 | var body = negationExpr.getBody(); | 694 | var body = negationExpr.getBody(); |
@@ -700,18 +697,11 @@ public class ModelInitializer { | |||
700 | throw new TracedException(extractedInner.body(), "Cannot negate literal"); | 697 | throw new TracedException(extractedInner.body(), "Cannot negate literal"); |
701 | } | 698 | } |
702 | var target = getPartialRelation(atom.getRelation()); | 699 | var target = getPartialRelation(atom.getRelation()); |
703 | Constraint constraint; | 700 | Constraint constraint = atom.isTransitiveClosure() ? getTransitiveWrapper(target) : target; |
704 | if (atom.isTransitiveClosure()) { | ||
705 | constraint = Query.of(target.name() + "#transitive", (builder, p1, p2) -> builder.clause( | ||
706 | target.callTransitive(p1, p2) | ||
707 | )).getDnf(); | ||
708 | } else { | ||
709 | constraint = target; | ||
710 | } | ||
711 | var negatedScope = extendScope(localScope, negationExpr.getImplicitVariables()); | 701 | var negatedScope = extendScope(localScope, negationExpr.getImplicitVariables()); |
712 | var argumentList = toArgumentList(atom.getArguments(), negatedScope, literals); | 702 | List<Variable> argumentList = toArgumentList(atom.getArguments(), negatedScope, literals); |
713 | var innerModality = extractedInner.modality().merge(outerModality.negate()); | 703 | var innerModality = extractedInner.modality().merge(outerModality.negate()); |
714 | literals.add(innerModality.wrapConstraint(constraint).call(CallPolarity.NEGATIVE, argumentList)); | 704 | literals.add(createNegationLiteral(innerModality, constraint, argumentList, localScope)); |
715 | } | 705 | } |
716 | case ComparisonExpr comparisonExpr -> { | 706 | case ComparisonExpr comparisonExpr -> { |
717 | var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()), | 707 | var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()), |
@@ -722,12 +712,63 @@ public class ModelInitializer { | |||
722 | default -> throw new TracedException( | 712 | default -> throw new TracedException( |
723 | comparisonExpr, "Unsupported operator"); | 713 | comparisonExpr, "Unsupported operator"); |
724 | }; | 714 | }; |
725 | literals.add(outerModality.createEquivalence(positive, argumentList.get(0), argumentList.get(1))); | 715 | literals.add(createEquivalenceLiteral(outerModality, positive, argumentList.get(0), argumentList.get(1), |
716 | localScope)); | ||
726 | } | 717 | } |
727 | default -> throw new TracedException(extractedOuter.body(), "Unsupported literal"); | 718 | default -> throw new TracedException(extractedOuter.body(), "Unsupported literal"); |
728 | } | 719 | } |
729 | } | 720 | } |
730 | 721 | ||
722 | private Constraint getTransitiveWrapper(Constraint target) { | ||
723 | return Query.of(target.name() + "#transitive", (builder, p1, p2) -> builder.clause( | ||
724 | target.callTransitive(p1, p2) | ||
725 | )).getDnf(); | ||
726 | } | ||
727 | |||
728 | private static Literal createNegationLiteral( | ||
729 | ConcreteModality innerModality, Constraint constraint, List<Variable> argumentList, | ||
730 | Map<tools.refinery.language.model.problem.Variable, ? extends Variable> localScope) { | ||
731 | if (innerModality.isSet()) { | ||
732 | boolean needsQuantification = false; | ||
733 | var filteredArguments = new LinkedHashSet<Variable>(); | ||
734 | for (var argument : argumentList) { | ||
735 | if (localScope.containsValue(argument)) { | ||
736 | filteredArguments.add(argument); | ||
737 | } else { | ||
738 | needsQuantification = true; | ||
739 | } | ||
740 | } | ||
741 | // If there are any quantified arguments, set a helper pattern to be lifted so that the appropriate | ||
742 | // {@code EXISTS} call are added by the {@code DnfLifter}. | ||
743 | if (needsQuantification) { | ||
744 | var filteredArgumentList = List.copyOf(filteredArguments); | ||
745 | var quantifiedConstraint = Dnf.builder(constraint.name() + "#quantified") | ||
746 | .parameters(filteredArgumentList) | ||
747 | .clause( | ||
748 | constraint.call(CallPolarity.POSITIVE, argumentList) | ||
749 | ) | ||
750 | .build(); | ||
751 | return innerModality.wrapConstraint(quantifiedConstraint) | ||
752 | .call(CallPolarity.NEGATIVE, filteredArgumentList); | ||
753 | } | ||
754 | } | ||
755 | return innerModality.wrapConstraint(constraint).call(CallPolarity.NEGATIVE, argumentList); | ||
756 | } | ||
757 | |||
758 | private Literal createEquivalenceLiteral( | ||
759 | ConcreteModality outerModality, boolean positive, Variable left, Variable right, | ||
760 | Map<tools.refinery.language.model.problem.Variable, ? extends Variable> localScope) { | ||
761 | if (!outerModality.isSet()) { | ||
762 | return new EquivalenceLiteral(positive, left, right); | ||
763 | } | ||
764 | if (positive) { | ||
765 | return outerModality.wrapConstraint(ReasoningAdapter.EQUALS_SYMBOL).call(left, right); | ||
766 | } | ||
767 | // Interpret {@code x != y} as {@code !equals(x, y)} at all times, even in modal operators. | ||
768 | return createNegationLiteral(outerModality.negate(), ReasoningAdapter.EQUALS_SYMBOL, List.of(left, right), | ||
769 | localScope); | ||
770 | } | ||
771 | |||
731 | private record ConcreteModality(@Nullable Concreteness concreteness, @Nullable Modality modality) { | 772 | private record ConcreteModality(@Nullable Concreteness concreteness, @Nullable Modality modality) { |
732 | public static final ConcreteModality NULL = new ConcreteModality((Concreteness) null, null); | 773 | public static final ConcreteModality NULL = new ConcreteModality((Concreteness) null, null); |
733 | 774 | ||
@@ -758,18 +799,14 @@ public class ModelInitializer { | |||
758 | } | 799 | } |
759 | 800 | ||
760 | public Constraint wrapConstraint(Constraint inner) { | 801 | public Constraint wrapConstraint(Constraint inner) { |
761 | if (concreteness != null && modality != null) { | 802 | if (isSet()) { |
762 | return new ModalConstraint(modality, concreteness, inner); | 803 | return new ModalConstraint(modality, concreteness, inner); |
763 | } | 804 | } |
764 | return inner; | 805 | return inner; |
765 | } | 806 | } |
766 | 807 | ||
767 | public Literal createEquivalence(boolean positive, Variable left, Variable right) { | 808 | public boolean isSet() { |
768 | if (concreteness != null && modality != null) { | 809 | return concreteness != null || modality != null; |
769 | var polarity = positive ? CallPolarity.POSITIVE : CallPolarity.NEGATIVE; | ||
770 | return wrapConstraint(ReasoningAdapter.EQUALS_SYMBOL).call(polarity, left, right); | ||
771 | } | ||
772 | return new EquivalenceLiteral(positive, left, right); | ||
773 | } | 810 | } |
774 | } | 811 | } |
775 | 812 | ||