refactor: DNF atoms

Restore count != capability.

Still needs semantics and tests for count atoms over partial models.

4 files changed, 76 insertions, 49 deletions

diff --git a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
index f514e96c..2a8429a3 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
+++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
@@ -72,7 +72,7 @@ NegativeLiteral:
         modality=Modality? "!" atom=Atom;
 
 enum ComparisonOp:
-        LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="==";
+        LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="==" | NOT_EQ="!=";
 
 CountLiteral:
         modality=Modality? "count" atom=Atom op=ComparisonOp threshold=INT;
diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/RelationInfo.java b/subprojects/language/src/main/java/tools/refinery/language/utils/RelationInfo.java
index ae56e3a5..2253d257 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/utils/RelationInfo.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/utils/RelationInfo.java
@@ -1,27 +1,24 @@
 package tools.refinery.language.utils;
 
+import tools.refinery.language.model.problem.*;
+
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.List;
 
-import tools.refinery.language.model.problem.Assertion;
-import tools.refinery.language.model.problem.Conjunction;
-import tools.refinery.language.model.problem.Multiplicity;
-import tools.refinery.language.model.problem.Parameter;
-import tools.refinery.language.model.problem.PredicateKind;
-import tools.refinery.language.model.problem.Relation;
-import tools.refinery.language.model.problem.TypeScope;
-
-public record RelationInfo(String name, PredicateKind kind, List<Parameter> parameters, Multiplicity multiplicity,
-                Relation opposite, Collection<Conjunction> bodies, Collection<Assertion> defaultAssertions,
-                Collection<Assertion> assertions, Collection<TypeScope> typeScopes) {
-        public RelationInfo(String name, PredicateKind kind, List<Parameter> parameters, Multiplicity multiplicity,
-                        Relation opposite, Collection<Conjunction> bodies) {
-                this(name, kind, parameters, multiplicity, opposite, bodies, new ArrayList<>(), new ArrayList<>(),
-                                new ArrayList<>());
+public record RelationInfo(String name, ContainmentRole containmentRole, List<Parameter> parameters,
+                                                   Multiplicity multiplicity, Relation opposite, Collection<Conjunction> bodies,
+                                                   Collection<Assertion> assertions, Collection<TypeScope> typeScopes) {
+        public RelationInfo(String name, ContainmentRole containmentRole, List<Parameter> parameters,
+                                                Multiplicity multiplicity, Relation opposite, Collection<Conjunction> bodies) {
+                this(name, containmentRole, parameters, multiplicity, opposite, bodies, new ArrayList<>(), new ArrayList<>());
         }
 
         public boolean hasDefinition() {
                 return bodies != null && !bodies.isEmpty();
         }
+
+        public int arity() {
+                return parameters.size();
+        }
 }
diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java b/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java
index a386db7f..210e96ab 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java
@@ -19,10 +19,12 @@ class SymbolCollector {
         private IQualifiedNameConverter qualifiedNameConverter;
 
         @Inject
-        ProblemDesugarer desugarer;
+        private ProblemDesugarer desugarer;
 
         private BuiltinSymbols builtinSymbols;
+
         private final Map<Node, NodeInfo> nodes = new LinkedHashMap<>();
+
         private final Map<Relation, RelationInfo> relations = new LinkedHashMap<>();
 
         public CollectedSymbols collectSymbols(Problem problem) {
@@ -54,9 +56,10 @@ class SymbolCollector {
         }
 
         private void collectPredicate(PredicateDefinition predicateDefinition) {
+                var predicateKind = predicateDefinition.getKind();
                 var info = new RelationInfo(getQualifiedNameString(predicateDefinition),
-                                predicateDefinition.getKind(),
-                                predicateDefinition.getParameters(), null, null, predicateDefinition.getBodies());
+                                ContainmentRole.fromPredicateKind(predicateKind), predicateDefinition.getParameters(), null, null,
+                                predicateDefinition.getBodies());
                 relations.put(predicateDefinition, info);
         }
 
@@ -65,10 +68,10 @@ class SymbolCollector {
                 // contained, including data types.
                 var contained =
                                 classDeclaration != builtinSymbols.node() && classDeclaration != builtinSymbols.domain();
-                var classKind = contained ? PredicateKind.CONTAINED : PredicateKind.DEFAULT;
+                var containmentRole = contained ? ContainmentRole.CONTAINED : ContainmentRole.NONE;
                 var instanceParameter = ProblemFactory.eINSTANCE.createParameter();
                 instanceParameter.setName("instance");
-                var classInfo = new RelationInfo(getQualifiedNameString(classDeclaration), classKind,
+                var classInfo = new RelationInfo(getQualifiedNameString(classDeclaration), containmentRole,
                                 List.of(instanceParameter), null, null, List.of());
                 relations.put(classDeclaration, classInfo);
                 collectReferences(classDeclaration);
@@ -76,9 +79,9 @@ class SymbolCollector {
 
         private void collectReferences(ClassDeclaration classDeclaration) {
                 for (var referenceDeclaration : classDeclaration.getReferenceDeclarations()) {
-                        var referenceKind = desugarer.isContainmentReference(referenceDeclaration) ?
-                                        PredicateKind.CONTAINMENT :
-                                        PredicateKind.DEFAULT;
+                        var referenceRole = desugarer.isContainmentReference(referenceDeclaration) ?
+                                        ContainmentRole.CONTAINMENT :
+                                        ContainmentRole.NONE;
                         var sourceParameter = ProblemFactory.eINSTANCE.createParameter();
                         sourceParameter.setName("source");
                         sourceParameter.setParameterType(classDeclaration);
@@ -91,7 +94,7 @@ class SymbolCollector {
                                 multiplicity = exactMultiplicity;
                         }
                         targetParameter.setParameterType(referenceDeclaration.getReferenceType());
-                        var referenceInfo = new RelationInfo(getQualifiedNameString(referenceDeclaration), referenceKind,
+                        var referenceInfo = new RelationInfo(getQualifiedNameString(referenceDeclaration), referenceRole,
                                         List.of(sourceParameter, targetParameter), multiplicity, referenceDeclaration.getOpposite(),
                                         List.of());
                         this.relations.put(referenceDeclaration, referenceInfo);
@@ -101,7 +104,7 @@ class SymbolCollector {
         private void collectEnum(EnumDeclaration enumDeclaration) {
                 var instanceParameter = ProblemFactory.eINSTANCE.createParameter();
                 instanceParameter.setName("instance");
-                var info = new RelationInfo(getQualifiedNameString(enumDeclaration), PredicateKind.DEFAULT,
+                var info = new RelationInfo(getQualifiedNameString(enumDeclaration), ContainmentRole.NONE,
                                 List.of(instanceParameter), null, null, List.of());
                 this.relations.put(enumDeclaration, info);
         }
@@ -172,6 +175,8 @@ class SymbolCollector {
                                 collectAssertion(assertion);
                         } else if (statement instanceof NodeValueAssertion nodeValueAssertion) {
                                 collectNodeValueAssertion(nodeValueAssertion);
+                        } else if (statement instanceof PredicateDefinition predicateDefinition) {
+                                collectPredicateAssertion(predicateDefinition);
                         } else if (statement instanceof ClassDeclaration classDeclaration) {
                                 collectClassAssertion(classDeclaration);
                         } else if (statement instanceof EnumDeclaration enumDeclaration) {
@@ -190,11 +195,7 @@ class SymbolCollector {
                         // Problem during editing. The errors can still be detected by the Problem validator.
                         return;
                 }
-                if (assertion.isDefault()) {
-                        relationInfo.defaultAssertions().add(assertion);
-                } else {
-                        relationInfo.assertions().add(assertion);
-                }
+                relationInfo.assertions().add(assertion);
                 for (var argument : assertion.getArguments()) {
                         if (argument instanceof ConstantAssertionArgument constantAssertionArgument) {
                                 var constantNode = constantAssertionArgument.getNode();
@@ -239,6 +240,14 @@ class SymbolCollector {
                 addAssertion(dataType, LogicValue.TRUE, node);
         }
 
+        private void collectPredicateAssertion(PredicateDefinition predicateDefinition) {
+                if (predicateDefinition.getKind() != PredicateKind.ERROR) {
+                        return;
+                }
+                int arity = predicateDefinition.getParameters().size();
+                addAssertion(predicateDefinition, LogicValue.FALSE, new Node[arity]);
+        }
+
         private void collectClassAssertion(ClassDeclaration classDeclaration) {
                 var node = classDeclaration.getNewNode();
                 if (node == null) {
@@ -259,8 +268,14 @@ class SymbolCollector {
                 var assertion = ProblemFactory.eINSTANCE.createAssertion();
                 assertion.setRelation(relation);
                 for (var node : nodes) {
-                        var argument = ProblemFactory.eINSTANCE.createNodeAssertionArgument();
-                        argument.setNode(node);
+                        AssertionArgument argument;
+                        if (node == null) {
+                                argument = ProblemFactory.eINSTANCE.createWildcardAssertionArgument();
+                        } else {
+                                var nodeArgument = ProblemFactory.eINSTANCE.createNodeAssertionArgument();
+                                nodeArgument.setNode(node);
+                                argument = nodeArgument;
+                        }
                         assertion.getArguments().add(argument);
                 }
                 assertion.setValue(logicValue);
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java
index e2e3218c..a05f3335 100644
--- a/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java
@@ -12,6 +12,7 @@ import org.junit.jupiter.params.provider.MethodSource;
 import tools.refinery.language.model.problem.*;
 import tools.refinery.language.model.tests.utils.ProblemParseHelper;
 import tools.refinery.language.tests.ProblemInjectorProvider;
+import tools.refinery.language.utils.ContainmentRole;
 import tools.refinery.language.utils.ProblemDesugarer;
 
 import java.util.stream.Stream;
@@ -61,7 +62,7 @@ class SymbolCollectorTest {
                 assertThat(collectedSymbols.relations(), hasKey(classDeclaration));
                 var classInfo = collectedSymbols.relations().get(classDeclaration);
                 assertThat(classInfo.parameters(), hasSize(1));
-                assertThat(classInfo.kind(), is(PredicateKind.CONTAINED));
+                assertThat(classInfo.containmentRole(), is(ContainmentRole.CONTAINED));
                 assertThat(classInfo.hasDefinition(), is(false));
                 var newNode = classDeclaration.getNewNode();
                 assertThat(collectedSymbols.nodes(), hasKey(newNode));
@@ -96,11 +97,11 @@ class SymbolCollectorTest {
                 var barInfo = collectedSymbols.relations().get(barReference);
                 var quuxReference = fooClass.reference("quux");
                 var quuxInfo = collectedSymbols.relations().get(quuxReference);
-                assertThat(barInfo.kind(), is(PredicateKind.DEFAULT));
+                assertThat(barInfo.containmentRole(), is(ContainmentRole.NONE));
                 assertThat(barInfo.opposite(), is(quuxReference));
                 assertThat(barInfo.multiplicity(), is(instanceOf(UnboundedMultiplicity.class)));
                 assertThat(barInfo.hasDefinition(), is(false));
-                assertThat(quuxInfo.kind(), is(PredicateKind.DEFAULT));
+                assertThat(quuxInfo.containmentRole(), is(ContainmentRole.NONE));
                 assertThat(quuxInfo.opposite(), is(barReference));
                 assertThat(quuxInfo.multiplicity(), is(instanceOf(ExactMultiplicity.class)));
                 assertThat(quuxInfo.multiplicity(), hasProperty("exactValue", is(1)));
@@ -115,8 +116,8 @@ class SymbolCollectorTest {
                                 }
                                 """);
                 var collectedSymbols = desugarer.collectSymbols(problem.get());
-                assertThat(collectedSymbols.relations().get(problem.findClass("Foo").reference("bar")).kind(),
-                                is(PredicateKind.CONTAINMENT));
+                assertThat(collectedSymbols.relations().get(problem.findClass("Foo").reference("bar")).containmentRole(),
+                                is(ContainmentRole.CONTAINMENT));
         }
 
         @Test
@@ -127,8 +128,8 @@ class SymbolCollectorTest {
                                 }
                                 """);
                 var collectedSymbols = desugarer.collectSymbols(problem.get());
-                assertThat(collectedSymbols.relations().get(problem.findClass("Foo").reference("bar")).kind(),
-                                is(PredicateKind.CONTAINMENT));
+                assertThat(collectedSymbols.relations().get(problem.findClass("Foo").reference("bar")).containmentRole(),
+                                is(ContainmentRole.CONTAINMENT));
         }
 
         @Test
@@ -141,27 +142,27 @@ class SymbolCollectorTest {
                 var collectedSymbols = desugarer.collectSymbols(problem.get());
                 var enumDeclaration = problem.findEnum("Foo");
                 var enumInfo = collectedSymbols.relations().get(enumDeclaration.get());
-                assertThat(enumInfo.kind(), is(PredicateKind.DEFAULT));
+                assertThat(enumInfo.containmentRole(), is(ContainmentRole.NONE));
                 assertThat(enumInfo.assertions(), assertsNode(enumDeclaration.literal("bar"), LogicValue.TRUE));
                 assertThat(enumInfo.assertions(), assertsNode(enumDeclaration.literal("quux"), LogicValue.TRUE));
         }
 
         @ParameterizedTest
         @MethodSource
-        void predicateTest(String keyword, PredicateKind kind) {
+        void predicateTest(String keyword, ContainmentRole containmentRole) {
                 var problem = parseHelper.parse(keyword + " foo(node x) <-> domain(x); data(x).");
                 var collectedSymbols = desugarer.collectSymbols(problem.get());
                 var predicateInfo = collectedSymbols.relations().get(problem.pred("foo").get());
-                assertThat(predicateInfo.kind(), is(kind));
+                assertThat(predicateInfo.containmentRole(), is(containmentRole));
                 assertThat(predicateInfo.parameters(), hasSize(1));
                 assertThat(predicateInfo.bodies(), hasSize(2));
                 assertThat(predicateInfo.hasDefinition(), is(true));
         }
 
         static Stream<Arguments> predicateTest() {
-                return Stream.of(Arguments.of("pred", PredicateKind.DEFAULT), Arguments.of("error", PredicateKind.ERROR),
-                                Arguments.of("contained", PredicateKind.CONTAINED), Arguments.of("containment",
-                                                PredicateKind.CONTAINMENT));
+                return Stream.of(Arguments.of("pred", ContainmentRole.NONE), Arguments.of("error", ContainmentRole.NONE),
+                                Arguments.of("contained", ContainmentRole.CONTAINED), Arguments.of("containment",
+                                                ContainmentRole.CONTAINMENT));
         }
 
         @ParameterizedTest
@@ -184,7 +185,7 @@ class SymbolCollectorTest {
                                 default foo(a): %s.
                                 """.formatted(keyword));
                 var collectedSymbols = desugarer.collectSymbols(problem.get());
-                assertThat(collectedSymbols.relations().get(problem.pred("foo").get()).defaultAssertions(),
+                assertThat(collectedSymbols.relations().get(problem.pred("foo").get()).assertions(),
                                 assertsNode(problem.node("a"), value));
         }
 
@@ -254,6 +255,10 @@ class SymbolCollectorTest {
                                 LogicValue.UNKNOWN));
         }
 
+        static Stream<Arguments> valueTypes() {
+                return Stream.of(Arguments.of("3", "int"), Arguments.of("3.14", "real"), Arguments.of("\"foo\"", "string"));
+        }
+
         @Test
         void invalidProblemTest() {
                 var problem = parseHelper.parse("""
@@ -265,8 +270,18 @@ class SymbolCollectorTest {
                 assertDoesNotThrow(() -> desugarer.collectSymbols(problem));
         }
 
-        static Stream<Arguments> valueTypes() {
-                return Stream.of(Arguments.of("3", "int"), Arguments.of("3.14", "real"), Arguments.of("\"foo\"", "string"));
+        @Test
+        void errorAssertionTest() {
+                var problem = parseHelper.parse("""
+                                error foo(node a, node b) <-> equals(a, b).
+                                """);
+                var collectedSymbols = desugarer.collectSymbols(problem.get());
+                var fooInfo = collectedSymbols.relations().get(problem.pred("foo").get());
+                assertThat(fooInfo.assertions(), hasSize(1));
+                var assertion = fooInfo.assertions().stream().findFirst().orElseThrow();
+                assertThat(assertion.getValue(), is(LogicValue.FALSE));
+                assertThat(assertion.getArguments(), hasSize(2));
+                assertThat(assertion.getArguments(), everyItem(instanceOf(WildcardAssertionArgument.class)));
         }
 
         private static Matcher<Iterable<? super Assertion>> assertsNode(Node node, LogicValue value) {