From 8183b588cf5bc665c0f96abc6d11b8dc70eecaa3 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 17 Feb 2023 17:35:48 +0100 Subject: feat: PartialInterpretation representations --- .../query/viatra/internal/pquery/Dnf2PQuery.java | 32 +++-------- .../store/partial/literal/ModalDnfCallLiteral.java | 30 ++++++++++ .../store/partial/literal/ModalLiteral.java | 45 +++++++++++++++ .../partial/literal/ModalRelationLiteral.java | 31 ++++++++++ .../refinery/store/partial/literal/Modality.java | 31 ++++++++++ .../store/partial/literal/PartialLiterals.java | 33 +++++++++++ .../partial/literal/PartialRelationLiteral.java | 27 +++++++++ .../partial/representation/AnyPartialFunction.java | 4 ++ .../partial/representation/AnyPartialSymbol.java | 11 ++++ .../partial/representation/PartialFunction.java | 32 +++++++++++ .../partial/representation/PartialRelation.java | 66 ++++++++++++++++++++++ .../partial/representation/PartialSymbol.java | 12 ++++ .../main/java/tools/refinery/store/query/Dnf.java | 12 ++-- .../java/tools/refinery/store/query/DnfUtils.java | 5 ++ .../refinery/store/query/literal/CallLiteral.java | 28 +++++---- .../store/query/literal/ConstantLiteral.java | 7 +++ .../store/query/literal/DnfCallLiteral.java | 12 +++- .../store/query/literal/EquivalenceLiteral.java | 8 +++ .../refinery/store/query/literal/Literal.java | 3 + .../refinery/store/query/literal/Modality.java | 22 -------- .../store/query/literal/RelationViewLiteral.java | 12 +++- .../refinery/store/query/view/RelationView.java | 12 ++-- .../store/representation/AbstractDomain.java | 29 ++++++++++ .../store/representation/AnyAbstractDomain.java | 7 +++ .../store/representation/TruthValueDomain.java | 60 ++++++++++++++++++++ .../refinery/store/util/CycleDetectingMapper.java | 51 +++++++++++++++++ 26 files changed, 546 insertions(+), 76 deletions(-) create mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/query/literal/Modality.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/representation/AnyAbstractDomain.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/Dnf2PQuery.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/Dnf2PQuery.java index 02e26bde..201e0ed0 100644 --- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/Dnf2PQuery.java +++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/Dnf2PQuery.java @@ -23,17 +23,16 @@ import tools.refinery.store.query.DnfUtils; import tools.refinery.store.query.Variable; import tools.refinery.store.query.literal.*; import tools.refinery.store.query.view.AnyRelationView; +import tools.refinery.store.util.CycleDetectingMapper; import java.util.*; import java.util.function.Function; -import java.util.stream.Collectors; public class Dnf2PQuery { private static final Object P_CONSTRAINT_LOCK = new Object(); - private final Set translating = new LinkedHashSet<>(); - - private final Map dnf2PQueryMap = new HashMap<>(); + private final CycleDetectingMapper mapper = new CycleDetectingMapper<>(Dnf::name, + this::doTranslate); private final Map view2WrapperMap = new LinkedHashMap<>(); @@ -47,24 +46,7 @@ public class Dnf2PQuery { } public RawPQuery translate(Dnf dnfQuery) { - if (translating.contains(dnfQuery)) { - var path = translating.stream().map(Dnf::name).collect(Collectors.joining(" -> ")); - throw new IllegalStateException("Circular reference %s -> %s detected".formatted(path, - dnfQuery.name())); - } - // We can't use computeIfAbsent here, because translating referenced queries calls this method in a reentrant - // way, which would cause a ConcurrentModificationException with computeIfAbsent. - var pQuery = dnf2PQueryMap.get(dnfQuery); - if (pQuery == null) { - translating.add(dnfQuery); - try { - pQuery = doTranslate(dnfQuery); - dnf2PQueryMap.put(dnfQuery, pQuery); - } finally { - translating.remove(dnfQuery); - } - } - return pQuery; + return mapper.map(dnfQuery); } public Map getRelationViews() { @@ -72,7 +54,7 @@ public class Dnf2PQuery { } public RawPQuery getAlreadyTranslated(Dnf dnfQuery) { - return dnf2PQueryMap.get(dnfQuery); + return mapper.getAlreadyMapped(dnfQuery); } private RawPQuery doTranslate(Dnf dnfQuery) { @@ -148,7 +130,7 @@ public class Dnf2PQuery { } private void translateRelationViewLiteral(RelationViewLiteral relationViewLiteral, PBody body) { - var substitution = translateSubstitution(relationViewLiteral.getSubstitution(), body); + var substitution = translateSubstitution(relationViewLiteral.getArguments(), body); var polarity = relationViewLiteral.getPolarity(); var relationView = relationViewLiteral.getTarget(); if (polarity == CallPolarity.POSITIVE) { @@ -205,7 +187,7 @@ public class Dnf2PQuery { } private void translateDnfCallLiteral(DnfCallLiteral dnfCallLiteral, PBody body) { - var variablesTuple = translateSubstitution(dnfCallLiteral.getSubstitution(), body); + var variablesTuple = translateSubstitution(dnfCallLiteral.getArguments(), body); var translatedReferred = translate(dnfCallLiteral.getTarget()); var polarity = dnfCallLiteral.getPolarity(); switch (polarity) { diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java new file mode 100644 index 00000000..8070726a --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java @@ -0,0 +1,30 @@ +package tools.refinery.store.partial.literal; + +import tools.refinery.store.query.Dnf; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.DnfCallLiteral; +import tools.refinery.store.query.literal.PolarLiteral; + +import java.util.List; +import java.util.Map; + +public class ModalDnfCallLiteral extends ModalLiteral implements PolarLiteral { + public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List arguments) { + super(polarity, modality, target, arguments); + } + + public ModalDnfCallLiteral(Modality modality, DnfCallLiteral baseLiteral) { + super(modality.commute(baseLiteral.getPolarity()), baseLiteral); + } + + @Override + public ModalDnfCallLiteral substitute(Map substitution) { + return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); + } + + @Override + public ModalDnfCallLiteral negate() { + return new ModalDnfCallLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); + } +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java new file mode 100644 index 00000000..a1b6c83e --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java @@ -0,0 +1,45 @@ +package tools.refinery.store.partial.literal; + +import tools.refinery.store.query.RelationLike; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallLiteral; +import tools.refinery.store.query.literal.CallPolarity; + +import java.util.List; +import java.util.Objects; + +public abstract class ModalLiteral extends CallLiteral { + private final Modality modality; + + protected ModalLiteral(CallPolarity polarity, Modality modality, T target, List arguments) { + super(polarity, target, arguments); + this.modality = modality; + } + + protected ModalLiteral(Modality modality, CallLiteral baseLiteral) { + this(baseLiteral.getPolarity(), commute(modality, baseLiteral.getPolarity()), baseLiteral.getTarget(), + baseLiteral.getArguments()); + } + + public Modality getModality() { + return modality; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + if (!super.equals(o)) return false; + ModalLiteral that = (ModalLiteral) o; + return modality == that.modality; + } + + @Override + public int hashCode() { + return Objects.hash(super.hashCode(), modality); + } + + private static Modality commute(Modality modality, CallPolarity polarity) { + return polarity.isPositive() ? modality : modality.negate(); + } +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java new file mode 100644 index 00000000..dbaa524f --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java @@ -0,0 +1,31 @@ +package tools.refinery.store.partial.literal; + +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.PolarLiteral; + +import java.util.List; +import java.util.Map; + +public final class ModalRelationLiteral extends ModalLiteral + implements PolarLiteral { + public ModalRelationLiteral(CallPolarity polarity, Modality modality, PartialRelation target, + List arguments) { + super(polarity, modality, target, arguments); + } + + public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) { + super(modality, baseLiteral); + } + + @Override + public ModalRelationLiteral substitute(Map substitution) { + return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution)); + } + + @Override + public ModalRelationLiteral negate() { + return new ModalRelationLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments()); + } +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java new file mode 100644 index 00000000..d647ef0a --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/Modality.java @@ -0,0 +1,31 @@ +package tools.refinery.store.partial.literal; + +import tools.refinery.store.query.literal.CallPolarity; + +import java.util.Locale; + +public enum Modality { + MUST, + MAY, + CURRENT; + + public Modality negate() { + return switch(this) { + case MUST -> MAY; + case MAY -> MUST; + case CURRENT -> CURRENT; + }; + } + + public Modality commute(CallPolarity polarity) { + if (polarity.isPositive()) { + return this; + } + return this.negate(); + } + + @Override + public String toString() { + return name().toLowerCase(Locale.ROOT); + } +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java new file mode 100644 index 00000000..51d388d3 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java @@ -0,0 +1,33 @@ +package tools.refinery.store.partial.literal; + +import tools.refinery.store.query.literal.DnfCallLiteral; + +public final class PartialLiterals { + private PartialLiterals() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public ModalRelationLiteral may(PartialRelationLiteral literal) { + return new ModalRelationLiteral(Modality.MAY, literal); + } + + public ModalRelationLiteral must(PartialRelationLiteral literal) { + return new ModalRelationLiteral(Modality.MUST, literal); + } + + public ModalRelationLiteral current(PartialRelationLiteral literal) { + return new ModalRelationLiteral(Modality.CURRENT, literal); + } + + public ModalDnfCallLiteral may(DnfCallLiteral literal) { + return new ModalDnfCallLiteral(Modality.MAY, literal); + } + + public ModalDnfCallLiteral must(DnfCallLiteral literal) { + return new ModalDnfCallLiteral(Modality.MUST, literal); + } + + public ModalDnfCallLiteral current(DnfCallLiteral literal) { + return new ModalDnfCallLiteral(Modality.CURRENT, literal); + } +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java new file mode 100644 index 00000000..dc1a1da3 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java @@ -0,0 +1,27 @@ +package tools.refinery.store.partial.literal; + +import tools.refinery.store.partial.representation.PartialRelation; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallLiteral; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.query.literal.PolarLiteral; + +import java.util.List; +import java.util.Map; + +public final class PartialRelationLiteral extends CallLiteral + implements PolarLiteral { + public PartialRelationLiteral(CallPolarity polarity, PartialRelation target, List substitution) { + super(polarity, target, substitution); + } + + @Override + public PartialRelationLiteral substitute(Map substitution) { + return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); + } + + @Override + public PartialRelationLiteral negate() { + return new PartialRelationLiteral(getPolarity().negate(), getTarget(), getArguments()); + } +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java new file mode 100644 index 00000000..1113245e --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java @@ -0,0 +1,4 @@ +package tools.refinery.store.partial.representation; + +public sealed interface AnyPartialFunction extends AnyPartialSymbol permits PartialFunction { +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java new file mode 100644 index 00000000..25096e74 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java @@ -0,0 +1,11 @@ +package tools.refinery.store.partial.representation; + +import tools.refinery.store.representation.AnyAbstractDomain; + +public sealed interface AnyPartialSymbol permits AnyPartialFunction, PartialSymbol { + String name(); + + int arity(); + + AnyAbstractDomain abstractDomain(); +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java new file mode 100644 index 00000000..3c186f6f --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java @@ -0,0 +1,32 @@ +package tools.refinery.store.partial.representation; + +import tools.refinery.store.representation.AbstractDomain; + +public record PartialFunction(String name, int arity, AbstractDomain abstractDomain) + implements AnyPartialFunction, PartialSymbol { + @Override + public A defaultValue() { + return null; + } + + @Override + public C defaultConcreteValue() { + return null; + } + + @Override + public boolean equals(Object o) { + return this == o; + } + + @Override + public int hashCode() { + // Compare by identity to make hash table lookups more efficient. + return System.identityHashCode(this); + } + + @Override + public String toString() { + return "%s/%d".formatted(name, arity); + } +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java new file mode 100644 index 00000000..127355ca --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java @@ -0,0 +1,66 @@ +package tools.refinery.store.partial.representation; + +import tools.refinery.store.partial.literal.ModalRelationLiteral; +import tools.refinery.store.partial.literal.PartialRelationLiteral; +import tools.refinery.store.query.RelationLike; +import tools.refinery.store.query.Variable; +import tools.refinery.store.query.literal.CallPolarity; +import tools.refinery.store.partial.literal.Modality; +import tools.refinery.store.representation.AbstractDomain; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.representation.TruthValueDomain; + +import java.util.List; + +public record PartialRelation(String name, int arity) implements PartialSymbol, RelationLike { + @Override + public AbstractDomain abstractDomain() { + return TruthValueDomain.INSTANCE; + } + + @Override + public TruthValue defaultValue() { + return TruthValue.FALSE; + } + + @Override + public Boolean defaultConcreteValue() { + return false; + } + + public ModalRelationLiteral call(CallPolarity polarity, Modality modality, List arguments) { + return new ModalRelationLiteral(polarity, modality, this, arguments); + } + + public PartialRelationLiteral call(CallPolarity polarity, List arguments) { + return new PartialRelationLiteral(polarity, this, arguments); + } + + public PartialRelationLiteral call(CallPolarity polarity, Variable... arguments) { + return call(polarity, List.of(arguments)); + } + + public PartialRelationLiteral call(Variable... arguments) { + return call(CallPolarity.POSITIVE, arguments); + } + + public PartialRelationLiteral callTransitive(Variable left, Variable right) { + return call(CallPolarity.TRANSITIVE, List.of(left, right)); + } + + @Override + public boolean equals(Object o) { + return this == o; + } + + @Override + public int hashCode() { + // Compare by identity to make hash table lookups more efficient. + return System.identityHashCode(this); + } + + @Override + public String toString() { + return "%s/%d".formatted(name, arity); + } +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java new file mode 100644 index 00000000..38533fa9 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java @@ -0,0 +1,12 @@ +package tools.refinery.store.partial.representation; + +import tools.refinery.store.representation.AbstractDomain; + +public sealed interface PartialSymbol extends AnyPartialSymbol permits PartialFunction, PartialRelation { + @Override + AbstractDomain abstractDomain(); + + A defaultValue(); + + C defaultConcreteValue(); +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java index 1eb9ac76..b080094f 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java @@ -74,16 +74,16 @@ public final class Dnf implements RelationLike { return clauses; } - public DnfCallLiteral call(CallPolarity polarity, List substitution) { - return new DnfCallLiteral(polarity, this, substitution); + public DnfCallLiteral call(CallPolarity polarity, List arguments) { + return new DnfCallLiteral(polarity, this, arguments); } - public DnfCallLiteral call(CallPolarity polarity, Variable... substitution) { - return call(polarity, List.of(substitution)); + public DnfCallLiteral call(CallPolarity polarity, Variable... arguments) { + return call(polarity, List.of(arguments)); } - public DnfCallLiteral call(Variable... substitution) { - return call(CallPolarity.POSITIVE, substitution); + public DnfCallLiteral call(Variable... arguments) { + return call(CallPolarity.POSITIVE, arguments); } public DnfCallLiteral callTransitive(Variable left, Variable right) { diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java b/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java index c7a2849c..17564d43 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/DnfUtils.java @@ -1,5 +1,6 @@ package tools.refinery.store.query; +import java.util.Map; import java.util.UUID; public final class DnfUtils { @@ -16,4 +17,8 @@ public final class DnfUtils { return originalName + uniqueString; } } + + public static Variable maybeSubstitute(Variable variable, Map substitution) { + return substitution.getOrDefault(variable, variable); + } } diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java index 59120434..5e1ae94d 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallLiteral.java @@ -1,28 +1,30 @@ package tools.refinery.store.query.literal; -import tools.refinery.store.query.Variable; +import tools.refinery.store.query.DnfUtils; import tools.refinery.store.query.RelationLike; +import tools.refinery.store.query.Variable; import java.util.List; +import java.util.Map; import java.util.Objects; import java.util.Set; public abstract class CallLiteral implements Literal { private final CallPolarity polarity; private final T target; - private final List substitution; + private final List arguments; - protected CallLiteral(CallPolarity polarity, T target, List substitution) { - if (substitution.size() != target.arity()) { + protected CallLiteral(CallPolarity polarity, T target, List arguments) { + if (arguments.size() != target.arity()) { throw new IllegalArgumentException("%s needs %d arguments, but got %s".formatted(target.name(), - target.arity(), substitution.size())); + target.arity(), arguments.size())); } if (polarity.isTransitive() && target.arity() != 2) { throw new IllegalArgumentException("Transitive closures can only take binary relations"); } this.polarity = polarity; this.target = target; - this.substitution = substitution; + this.arguments = arguments; } public CallPolarity getPolarity() { @@ -33,28 +35,32 @@ public abstract class CallLiteral implements Literal { return target; } - public List getSubstitution() { - return substitution; + public List getArguments() { + return arguments; } @Override public void collectAllVariables(Set variables) { if (polarity.isPositive()) { - variables.addAll(substitution); + variables.addAll(arguments); } } + protected List substituteArguments(Map substitution) { + return arguments.stream().map(variable -> DnfUtils.maybeSubstitute(variable, substitution)).toList(); + } + @Override public boolean equals(Object o) { if (this == o) return true; if (o == null || getClass() != o.getClass()) return false; CallLiteral callAtom = (CallLiteral) o; return polarity == callAtom.polarity && Objects.equals(target, callAtom.target) && - Objects.equals(substitution, callAtom.substitution); + Objects.equals(arguments, callAtom.arguments); } @Override public int hashCode() { - return Objects.hash(polarity, target, substitution); + return Objects.hash(polarity, target, arguments); } } diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java index 41426fdd..746d23af 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java @@ -1,7 +1,9 @@ package tools.refinery.store.query.literal; +import tools.refinery.store.query.DnfUtils; import tools.refinery.store.query.Variable; +import java.util.Map; import java.util.Set; public record ConstantLiteral(Variable variable, int nodeId) implements Literal { @@ -9,4 +11,9 @@ public record ConstantLiteral(Variable variable, int nodeId) implements Literal public void collectAllVariables(Set variables) { variables.add(variable); } + + @Override + public ConstantLiteral substitute(Map substitution) { + return new ConstantLiteral(DnfUtils.maybeSubstitute(variable, substitution), nodeId); + } } diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java index 86149b33..40499222 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java @@ -4,14 +4,20 @@ import tools.refinery.store.query.Dnf; import tools.refinery.store.query.Variable; import java.util.List; +import java.util.Map; public final class DnfCallLiteral extends CallLiteral implements PolarLiteral { - public DnfCallLiteral(CallPolarity polarity, Dnf target, List substitution) { - super(polarity, target, substitution); + public DnfCallLiteral(CallPolarity polarity, Dnf target, List arguments) { + super(polarity, target, arguments); + } + + @Override + public DnfCallLiteral substitute(Map substitution) { + return new DnfCallLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); } @Override public DnfCallLiteral negate() { - return new DnfCallLiteral(getPolarity().negate(), getTarget(), getSubstitution()); + return new DnfCallLiteral(getPolarity().negate(), getTarget(), getArguments()); } } diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java index 75afd50b..5fee54b1 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java @@ -1,7 +1,9 @@ package tools.refinery.store.query.literal; +import tools.refinery.store.query.DnfUtils; import tools.refinery.store.query.Variable; +import java.util.Map; import java.util.Set; public record EquivalenceLiteral(boolean positive, Variable left, Variable right) @@ -16,4 +18,10 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right public EquivalenceLiteral negate() { return new EquivalenceLiteral(!positive, left, right); } + + @Override + public EquivalenceLiteral substitute(Map substitution) { + return new EquivalenceLiteral(positive, DnfUtils.maybeSubstitute(left, substitution), + DnfUtils.maybeSubstitute(right, substitution)); + } } diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java index 676ac7fd..e0f5f605 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literal.java @@ -2,8 +2,11 @@ package tools.refinery.store.query.literal; import tools.refinery.store.query.Variable; +import java.util.Map; import java.util.Set; public interface Literal { void collectAllVariables(Set variables); + + Literal substitute(Map substitution); } diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Modality.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/Modality.java deleted file mode 100644 index 93826161..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Modality.java +++ /dev/null @@ -1,22 +0,0 @@ -package tools.refinery.store.query.literal; - -import java.util.Locale; - -public enum Modality { - MUST, - MAY, - CURRENT; - - public Modality negate() { - return switch(this) { - case MUST -> MAY; - case MAY -> MUST; - case CURRENT -> CURRENT; - }; - } - - @Override - public String toString() { - return name().toLowerCase(Locale.ROOT); - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java index 7fa99abb..4718b550 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java @@ -4,15 +4,21 @@ import tools.refinery.store.query.Variable; import tools.refinery.store.query.view.AnyRelationView; import java.util.List; +import java.util.Map; public final class RelationViewLiteral extends CallLiteral implements PolarLiteral { - public RelationViewLiteral(CallPolarity polarity, AnyRelationView target, List substitution) { - super(polarity, target, substitution); + public RelationViewLiteral(CallPolarity polarity, AnyRelationView target, List arguments) { + super(polarity, target, arguments); + } + + @Override + public RelationViewLiteral substitute(Map substitution) { + return new RelationViewLiteral(getPolarity(), getTarget(), substituteArguments(substitution)); } @Override public RelationViewLiteral negate() { - return new RelationViewLiteral(getPolarity().negate(), getTarget(), getSubstitution()); + return new RelationViewLiteral(getPolarity().negate(), getTarget(), getArguments()); } } diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java index 0bea962d..6accd27a 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java @@ -51,16 +51,16 @@ public abstract non-sealed class RelationView implements AnyRelationView { return (() -> new CursorAsIterator<>(model.getInterpretation(symbol).getAll(), this::forwardMap, this::filter)); } - public RelationViewLiteral call(CallPolarity polarity, List substitution) { - return new RelationViewLiteral(polarity, this, substitution); + public RelationViewLiteral call(CallPolarity polarity, List arguments) { + return new RelationViewLiteral(polarity, this, arguments); } - public RelationViewLiteral call(CallPolarity polarity, Variable... substitution) { - return call(polarity, List.of(substitution)); + public RelationViewLiteral call(CallPolarity polarity, Variable... arguments) { + return call(polarity, List.of(arguments)); } - public RelationViewLiteral call(Variable... substitution) { - return call(CallPolarity.POSITIVE, substitution); + public RelationViewLiteral call(Variable... arguments) { + return call(CallPolarity.POSITIVE, arguments); } public RelationViewLiteral callTransitive(Variable left, Variable right) { diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java new file mode 100644 index 00000000..18903ead --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java @@ -0,0 +1,29 @@ +package tools.refinery.store.representation; + +import java.util.Optional; + +public non-sealed interface AbstractDomain extends AnyAbstractDomain { + @Override + Class abstractType(); + + @Override + Class concreteType(); + + A toAbstract(C concreteValue); + + Optional toConcrete(A abstractValue); + + default boolean isConcrete(A abstractValue) { + return toConcrete(abstractValue).isPresent(); + } + + boolean isRefinement(A originalValue, A refinedValue); + + A commonRefinement(A leftValue, A rightValue); + + A commonAncestor(A leftValue, A rightValue); + + A unknown(); + + boolean isError(A abstractValue); +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/AnyAbstractDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/AnyAbstractDomain.java new file mode 100644 index 00000000..4c428a1e --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/AnyAbstractDomain.java @@ -0,0 +1,7 @@ +package tools.refinery.store.representation; + +public sealed interface AnyAbstractDomain permits AbstractDomain { + Class abstractType(); + + Class concreteType(); +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java new file mode 100644 index 00000000..29858bce --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java @@ -0,0 +1,60 @@ +package tools.refinery.store.representation; + +import java.util.Optional; + +public final class TruthValueDomain implements AbstractDomain { + public static final TruthValueDomain INSTANCE = new TruthValueDomain(); + + private TruthValueDomain() { + } + + @Override + public Class abstractType() { + return null; + } + + @Override + public Class concreteType() { + return null; + } + + @Override + public TruthValue toAbstract(Boolean concreteValue) { + return null; + } + + @Override + public Optional toConcrete(TruthValue abstractValue) { + return Optional.empty(); + } + + @Override + public boolean isConcrete(TruthValue abstractValue) { + return AbstractDomain.super.isConcrete(abstractValue); + } + + @Override + public boolean isRefinement(TruthValue originalValue, TruthValue refinedValue) { + return false; + } + + @Override + public TruthValue commonRefinement(TruthValue leftValue, TruthValue rightValue) { + return null; + } + + @Override + public TruthValue commonAncestor(TruthValue leftValue, TruthValue rightValue) { + return null; + } + + @Override + public TruthValue unknown() { + return null; + } + + @Override + public boolean isError(TruthValue abstractValue) { + return false; + } +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java b/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java new file mode 100644 index 00000000..e4b462f0 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java @@ -0,0 +1,51 @@ +package tools.refinery.store.util; + +import java.util.HashMap; +import java.util.LinkedHashSet; +import java.util.Map; +import java.util.Set; +import java.util.function.Function; +import java.util.stream.Collectors; + +public class CycleDetectingMapper { + private static final String SEPARATOR = " -> "; + + private final Function getName; + + private final Function doMap; + + private final Set inProgress = new LinkedHashSet<>(); + + private final Map results = new HashMap<>(); + + public CycleDetectingMapper(Function getName, Function doMap) { + this.getName = getName; + this.doMap = doMap; + } + + public R map(T input) { + if (inProgress.contains(input)) { + var path = inProgress.stream().map(getName).collect(Collectors.joining(SEPARATOR)); + throw new IllegalArgumentException("Circular reference %s%s%s detected".formatted(path, SEPARATOR, + getName.apply(input))); + } + // We can't use computeIfAbsent here, because translating referenced queries calls this method in a reentrant + // way, which would cause a ConcurrentModificationException with computeIfAbsent. + @SuppressWarnings("squid:S3824") + var result = results.get(input); + if (result == null) { + inProgress.add(input); + try { + result = doMap.apply(input); + results.put(input, result); + } finally { + inProgress.remove(input); + } + } + return result; + } + + public R getAlreadyMapped(T input) { + return results.get(input); + } +} -- cgit v1.2.3-70-g09d2