feat: base predicates

5 files changed, 252 insertions, 7 deletions

diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java
index 7a959991..4471b193 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java
@@ -21,9 +21,9 @@ class DirectedCrossReferenceRefiner extends ConcreteSymbolRefiner<TruthValue, Bo
         private PartialInterpretationRefiner<TruthValue, Boolean> sourceRefiner;
         private PartialInterpretationRefiner<TruthValue, Boolean> targetRefiner;
 
-        public DirectedCrossReferenceRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
-                                                                                 Symbol<TruthValue> concreteSymbol, PartialRelation sourceType,
-                                                                                 PartialRelation targetType) {
+        protected DirectedCrossReferenceRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                                                                        Symbol<TruthValue> concreteSymbol, PartialRelation sourceType,
+                                                                                        PartialRelation targetType) {
                 super(adapter, partialSymbol, concreteSymbol);
                 this.sourceType = sourceType;
                 this.targetType = targetType;
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java
index 79251d13..93ed30f6 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java
@@ -21,8 +21,9 @@ class UndirectedCrossReferenceRefiner extends ConcreteSymbolRefiner<TruthValue,
         private final PartialRelation sourceType;
         private PartialInterpretationRefiner<TruthValue, Boolean> sourceRefiner;
 
-        public UndirectedCrossReferenceRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
-                                                                                   Symbol<TruthValue> concreteSymbol, PartialRelation sourceType) {
+        protected UndirectedCrossReferenceRefiner(ReasoningAdapter adapter,
+                                              PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                                                                          Symbol<TruthValue> concreteSymbol, PartialRelation sourceType) {
                 super(adapter, partialSymbol, concreteSymbol);
                 this.sourceType = sourceType;
         }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/BasePredicateTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/BasePredicateTranslator.java
new file mode 100644
index 00000000..198bdbfb
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/BasePredicateTranslator.java
@@ -0,0 +1,141 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.predicate;
+
+import tools.refinery.logic.dnf.AbstractQueryBuilder;
+import tools.refinery.logic.dnf.Query;
+import tools.refinery.logic.literal.Literal;
+import tools.refinery.logic.term.NodeVariable;
+import tools.refinery.logic.term.truthvalue.TruthValue;
+import tools.refinery.store.dse.propagation.PropagationBuilder;
+import tools.refinery.store.dse.transition.Rule;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
+import tools.refinery.store.query.view.ForbiddenView;
+import tools.refinery.store.reasoning.lifting.DnfLifter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+import tools.refinery.store.reasoning.translator.RoundingMode;
+import tools.refinery.store.reasoning.translator.TranslationException;
+import tools.refinery.store.representation.Symbol;
+
+import java.util.ArrayList;
+import java.util.List;
+
+import static tools.refinery.logic.literal.Literals.not;
+import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.*;
+import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW;
+
+public class BasePredicateTranslator implements ModelStoreConfiguration {
+        private final PartialRelation predicate;
+        private final List<PartialRelation> parameterTypes;
+        private final TruthValue defaultValue;
+        private final boolean partial;
+        private final Symbol<TruthValue> symbol;
+
+        public BasePredicateTranslator(PartialRelation predicate, List<PartialRelation> parameterTypes,
+                                                                   TruthValue defaultValue, boolean partial) {
+                this.predicate = predicate;
+                this.parameterTypes = parameterTypes;
+                this.defaultValue = defaultValue;
+                this.partial = partial;
+                symbol = Symbol.of(predicate.name(), predicate.arity(), TruthValue.class, defaultValue);
+        }
+
+        @Override
+        public void apply(ModelStoreBuilder storeBuilder) {
+                int arity = predicate.arity();
+                if (arity != parameterTypes.size()) {
+                        throw new TranslationException(predicate,
+                                        "Expected %d parameter type for base predicate %s, got %d instead"
+                                                        .formatted(arity, predicate, parameterTypes.size()));
+                }
+                if (defaultValue.must()) {
+                        throw new TranslationException(predicate, "Unsupported default value %s for base predicate %s"
+                                        .formatted(defaultValue, predicate));
+                }
+                var translator = PartialRelationTranslator.of(predicate);
+                translator.symbol(symbol);
+                if (defaultValue.may()) {
+                        configureWithDefaultUnknown(translator);
+                } else {
+                        configureWithDefaultFalse(storeBuilder);
+                }
+                translator.refiner(PredicateRefiner.of(symbol, parameterTypes));
+                if (partial) {
+                        translator.roundingMode(RoundingMode.NONE);
+                } else {
+                        translator.decision(Rule.of(predicate.name(), builder -> {
+                                var parameters = createParameters(builder);
+                                var literals = new ArrayList<Literal>(arity + 2);
+                                literals.add(may(predicate.call(parameters)));
+                                literals.add(not(candidateMust(predicate.call(parameters))));
+                                for (int i = 0; i < arity; i++) {
+                                        literals.add(not(MULTI_VIEW.call(parameters[i])));
+                                }
+                                builder.clause(literals);
+                                builder.action(add(predicate, parameters));
+                        }));
+                }
+                storeBuilder.with(translator);
+        }
+
+        private NodeVariable[] createParameters(AbstractQueryBuilder<?> builder) {
+                int arity = predicate.arity();
+                var parameters = new NodeVariable[arity];
+                for (int i = 0; i < arity; i++) {
+                        parameters[i] = builder.parameter("p" + (i + 1));
+                }
+                return parameters;
+        }
+
+        private void configureWithDefaultUnknown(PartialRelationTranslator translator) {
+                var name = predicate.name();
+                var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL);
+                int arity = predicate.arity();
+                var forbiddenView = new ForbiddenView(symbol);
+                translator.may(Query.of(mayName, builder -> {
+                        var parameters = createParameters(builder);
+                        var literals = new ArrayList<Literal>(arity + 1);
+                        for (int i = 0; i < arity; i++) {
+                                literals.add(may(parameterTypes.get(i).call(parameters[i])));
+                        }
+                        literals.add(not(forbiddenView.call(parameters)));
+                        builder.clause(literals);
+                }));
+                if (partial) {
+                        var candidateMayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.CANDIDATE);
+                        translator.candidateMay(Query.of(candidateMayName, builder -> {
+                                var parameters = createParameters(builder);
+                                var literals = new ArrayList<Literal>(arity + 1);
+                                for (int i = 0; i < arity; i++) {
+                                        literals.add(candidateMay(parameterTypes.get(i).call(parameters[i])));
+                                }
+                                literals.add(not(forbiddenView.call(parameters)));
+                                builder.clause(literals);
+                        }));
+                }
+        }
+
+        private void configureWithDefaultFalse(ModelStoreBuilder storeBuilder) {
+                var name = predicate.name();
+                // Fail if there is no {@link PropagationBuilder}, since it is required for soundness.
+                var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class);
+                propagationBuilder.rule(Rule.of(name + "#invalidLink", builder -> {
+                        var parameters = createParameters(builder);
+                        int arity = parameters.length;
+                        for (int i = 0; i < arity; i++) {
+                                builder.clause(
+                                                may(predicate.call(parameters)),
+                                                not(may(parameterTypes.get(i).call(parameters[i])))
+                                );
+                        }
+                }));
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateRefiner.java
new file mode 100644
index 00000000..0fccced2
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateRefiner.java
@@ -0,0 +1,94 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.predicate;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.logic.term.truthvalue.TruthValue;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.List;
+import java.util.Objects;
+
+class PredicateRefiner extends ConcreteSymbolRefiner<TruthValue, Boolean> {
+        private final List<PartialRelation> parameterTypes;
+        private @Nullable PartialInterpretationRefiner<TruthValue, Boolean>[] parameterTypeRefiners;
+
+        protected PredicateRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                                           Symbol<TruthValue> concreteSymbol, List<PartialRelation> parameterTypes) {
+                super(adapter, partialSymbol, concreteSymbol);
+                this.parameterTypes = parameterTypes;
+        }
+
+        @Override
+        public void afterCreate() {
+                int arity = parameterTypes.size();
+                // Generic array creation.
+                @SuppressWarnings("unchecked")
+                PartialInterpretationRefiner<TruthValue, Boolean>[] array = new PartialInterpretationRefiner[arity];
+                parameterTypeRefiners = array;
+                var adapter = getAdapter();
+                for (int i = 0; i < arity; i++) {
+                        var parameterType = parameterTypes.get(i);
+                        if (parameterType != null) {
+                                array[i] = adapter.getRefiner(parameterType);
+                        }
+                }
+        }
+
+        @Override
+        public boolean merge(Tuple key, TruthValue value) {
+                var currentValue = get(key);
+                var mergedValue = currentValue.meet(value);
+                if (!Objects.equals(currentValue, mergedValue)) {
+                        put(key, mergedValue);
+                }
+                // Avoid cyclic propagation between parameter types by avoiding propagation after reaching a fixed point.
+                if (mergedValue.must() && !currentValue.must()) {
+                        return refineParameters(key);
+                }
+                return true;
+        }
+
+        @Override
+        public void afterInitialize(ModelSeed modelSeed) {
+                var predicate = getPartialSymbol();
+                var cursor = modelSeed.getCursor(predicate);
+                while (cursor.move()) {
+                        var value = cursor.getValue();
+                        if (value.must()) {
+                                var key = cursor.getKey();
+                                if (!refineParameters(key)) {
+                                        throw new IllegalArgumentException("Failed to merge parameter types of predicate %s for key %s"
+                                                        .formatted(predicate, key));
+                                }
+                        }
+                }
+        }
+
+        private boolean refineParameters(Tuple key) {
+                int arity = parameterTypeRefiners.length;
+                for (int i = 0; i < arity; i++) {
+                        var refiner = parameterTypeRefiners[i];
+                        if (refiner != null && !refiner.merge(Tuple.of(key.get(i)), TruthValue.TRUE)) {
+                                return false;
+                        }
+                }
+                return true;
+        }
+
+        public static Factory<TruthValue, Boolean> of(Symbol<TruthValue> concreteSymbol,
+                                                                                                  List<PartialRelation> parameterTypes) {
+                return (adapter, partialSymbol) -> new PredicateRefiner(adapter, partialSymbol, concreteSymbol,
+                                parameterTypes);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateTranslator.java
index 010ce977..8dd9cff6 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/predicate/PredicateTranslator.java
@@ -21,6 +21,9 @@ import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
 import tools.refinery.store.reasoning.translator.TranslationException;
 import tools.refinery.store.representation.Symbol;
 
+import java.util.List;
+import java.util.Objects;
+
 import static tools.refinery.logic.literal.Literals.not;
 import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
 import static tools.refinery.store.reasoning.literal.PartialLiterals.must;
@@ -30,9 +33,11 @@ public class PredicateTranslator implements ModelStoreConfiguration {
         private final RelationalQuery query;
         private final boolean mutable;
         private final TruthValue defaultValue;
+        private final List<PartialRelation> parameterTypes;
 
-        public PredicateTranslator(PartialRelation relation, RelationalQuery query, boolean mutable,
-                                                           TruthValue defaultValue) {
+        public PredicateTranslator(PartialRelation relation, RelationalQuery query, List<PartialRelation> parameterTypes,
+                                                           boolean mutable, TruthValue defaultValue) {
+                this.parameterTypes = parameterTypes;
                 if (relation.arity() != query.arity()) {
                         throw new TranslationException(relation, "Expected arity %d query for partial relation %s, got %d instead"
                                         .formatted(relation.arity(), relation, query.arity()));
@@ -78,6 +83,10 @@ public class PredicateTranslator implements ModelStoreConfiguration {
                                         .clause(mayLiterals)
                                         .build();
                         translator.may(may);
+
+                        if (parameterTypes != null && parameterTypes.stream().anyMatch(Objects::nonNull)) {
+                                translator.refiner(PredicateRefiner.of(symbol, parameterTypes));
+                        }
                 } else if (defaultValue.may()) {
                         // If all values are permitted, we don't need to check for any forbidden values in the model.
                         // If the result of this predicate of {@code ERROR}, some other partial relation (that we check for)