Add cat parsing support for recursive sets.

Author: xeren

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java

@@ -255,6 +255,7 @@ public EdgeEncoder edge(Relation relation) {
         EventGraph must = k.getMustSet();
         EdgeEncoder variable = relation.getDefinition().getEdgeVariableEncoder(this);
         return (e1, e2) -> {
+            checkArgument(!relation.isSet() || e1.equals(e2), "Cannot encode pairs of events in an event set");
             if (!may.contains(e1, e2)) {
                 return booleanFormulaManager.makeFalse();
             }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java

@@ -157,8 +157,8 @@ public Void visitLetRecDefinition(LetRecDefinitionContext ctx) {
         final int recSize = ctx.letRecAndDefinition().size() + 1;
         final Relation[] recursiveGroup = new Relation[recSize];
         final String[] lhsNames = new String[recSize];
-
-        // Create the recursive relations
+        final ExpressionContext[] rhsContexts = new ExpressionContext[recSize];
+        // Recompose the syntax.
         for (int i = 0; i < recSize; i++) {
             // First relation needs special treatment due to syntactic difference
             final String relName = i == 0 ? ctx.n.getText() : ctx.letRecAndDefinition(i - 1).n.getText();
@@ -167,14 +167,18 @@ public Void visitLetRecDefinition(LetRecDefinitionContext ctx) {
                 throw new MalformedMemoryModelException(errorMsg);
             }
             lhsNames[i] = relName;
-            recursiveGroup[i] = wmm.newRelation(createUniqueName(relName));
+            rhsContexts[i] = i == 0 ? ctx.e : ctx.letRecAndDefinition(i - 1).e;
+        }
+        // Create the recursive relations.
+        for (int i = 0; i < recSize; i++) {
+            final Relation.Arity arity = rhsContexts[i].accept(new ArityInspector());
+            recursiveGroup[i] = wmm.newRelation(createUniqueName(lhsNames[i]), arity);
             recursiveGroup[i].setRecursive();
-            namespace.put(relName, recursiveGroup[i]);
+            namespace.put(lhsNames[i], recursiveGroup[i]);
         }
-
-        // Parse recursive definitions
+        // Parse recursive definitions.
         for (int i = 0; i < recSize; i++) {
-            final ExpressionContext rhs = i == 0 ? ctx.e : ctx.letRecAndDefinition(i - 1).e;
+            final ExpressionContext rhs = rhsContexts[i];
             final Relation lhs = recursiveGroup[i];
             setRelationToBeDefined(lhs);
             final Relation parsedRhs = parseAsRelation(rhs);
@@ -326,15 +330,13 @@ public Relation visitExprTransRef(ExprTransRefContext c) {
 
     @Override
     public Relation visitExprDomain(ExprDomainContext c) {
-        checkNoRecursion(c);
         Relation r0 = wmm.newSet();
         Relation r1 = parseAsRelation(c.e);
         return addDefinition(new Domain(r0, r1));
     }
 
     @Override
     public Relation visitExprRange(ExprRangeContext c) {
-        checkNoRecursion(c);
         Relation r0 = wmm.newSet();
         Relation r1 = parseAsRelation(c.e);
         return addDefinition(new Range(r0, r1));
@@ -407,5 +409,69 @@ private static CatParser getParser(CharStream input) {
         parser.addErrorListener(new DiagnosticErrorListener(true));
         return parser;
     }
+
+    private final class ArityInspector extends CatBaseVisitor<Relation.Arity> {
+
+        private ArityInspector() {}
+
+        @Override
+        public Relation.Arity visitExprBasic(ExprBasicContext c) {
+            final Object object = namespace.get(c.n.getText());
+            return object instanceof Relation r ? r.getArity() : null;
+        }
+
+        @Override
+        public Relation.Arity visitExprDomain(ExprDomainContext c) {
+            return Relation.Arity.UNARY;
+        }
+
+        @Override
+        public Relation.Arity visitExprRange(ExprRangeContext c) {
+            return Relation.Arity.UNARY;
+        }
+
+        @Override
+        public Relation.Arity visitExprCartesian(ExprCartesianContext c) {
+            return Relation.Arity.BINARY;
+        }
+
+        @Override
+        public Relation.Arity visitExprComposition(ExprCompositionContext c) {
+            return Relation.Arity.BINARY;
+        }
+
+        @Override
+        public Relation.Arity visitExprIdentity(ExprIdentityContext c) {
+            return Relation.Arity.BINARY;
+        }
+
+        @Override
+        public Relation.Arity visitExprUnion(ExprUnionContext c) {
+            return join(c.e1, c.e2);
+        }
+
+        @Override
+        public Relation.Arity visitExprIntersection(ExprIntersectionContext c) {
+            return join(c.e1, c.e2);
+        }
+
+        @Override
+        public Relation.Arity visitExprMinus(ExprMinusContext c) {
+            return join(c.e1, c.e2);
+        }
+
+        private Relation.Arity join(ExpressionContext e1, ExpressionContext e2) {
+            final Relation.Arity k1 = e1.accept(this);
+            final Relation.Arity k2 = e2.accept(this);
+            checkCompatible(k1, k2);
+            return k1 == null ? k2 : k1;
+        }
+
+        private static void checkCompatible(Relation.Arity k1, Relation.Arity k2) {
+            if (k1 != null && k2 != null && !k1.equals(k2)) {
+                throw new ParsingException("Incompatible kinds %s and %s".formatted(k1, k2));
+            }
+        }
+    }
 }
 

dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java

@@ -7,7 +7,7 @@
 import com.dat3m.dartagnan.wmm.Relation;
 import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis;
 
-// A default implementation for any encoded relation, e.g. base relations or non-base but cut relations.
+// A default implementation for any encoded set, e.g. base sets or non-base but cut sets.
 public class DynamicDefaultWMMSet extends MaterializedWMMSet {
 
     private final Relation relation;

dartagnan/src/test/java/com/dat3m/dartagnan/parsers/cat/CatParserTest.java

@@ -0,0 +1,19 @@
+package com.dat3m.dartagnan.parsers.cat;
+
+import com.dat3m.dartagnan.wmm.Wmm;
+import org.junit.Test;
+
+import static org.junit.Assert.assertTrue;
+
+public class CatParserTest {
+
+    @Test
+    public void recursiveSet() {
+        final String text = """
+                let rec r0 = domain(loc & ([W]; po; [F]; po; [R])) | domain([r0]; addr)
+                acyclic (po & loc) | addr | data | ctrl | rf | co | fr | po ; [r0]
+                """;
+        final Wmm memoryModel = new ParserCat().parse(text);
+        assertTrue(memoryModel.getRelation("r0").isRecursive());
+    }
+}