Support unary predicates in cat

dartagnan/src/main/antlr4/Cat.g4

@@ -48,12 +48,13 @@ expression
     |   e1 = expression BSLASH e2 = expression                          # exprMinus
     |   e1 = expression SEMI e2 = expression                            # exprComposition
     |   e1 = expression BAR e2 = expression                             # exprUnion
-    |   LBRAC DOMAIN LPAR e = expression RPAR RBRAC                     # exprDomainIdentity
-    |   LBRAC RANGE LPAR e = expression RPAR RBRAC                      # exprRangeIdentity
+    |   DOMAIN LPAR e = expression RPAR                                 # exprDomain
+    |   RANGE LPAR e = expression RPAR                                  # exprRange
     |   (TOID LPAR e = expression RPAR | LBRAC e = expression RBRAC)    # exprIdentity
     |   LPAR e = expression RPAR                                        # expr
     |   n = NAME                                                        # exprBasic
-    |   call = NEW LPAR RPAR                                            # exprNew
+    |   NEW_SET LPAR RPAR                                               # exprNewSet
+    |   NEW_RELATION LPAR RPAR                                          # exprNewRelation
     |   call = NAME LPAR args = argumentList RPAR                       # exprCall
     ;
 
@@ -103,9 +104,10 @@ LBRAC   :   '[';
 RBRAC   :   ']';
 COMMA   :   ',';
 
-DOMAIN      :   'domain';
-RANGE       :   'range';
-NEW         :   'new';
+DOMAIN       :   'domain';
+RANGE        :   'range';
+NEW_SET      :   'newSet';
+NEW_RELATION :   'newRelation';
 
 FLAG       :   'flag';
 UNDEFINED  :   'undefined_unless';

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

@@ -84,40 +84,51 @@ public Map<Relation, EventGraph> visitComposition(Composition comp) {
     }
 
     @Override
-    public Map<Relation, EventGraph> visitDomainIdentity(DomainIdentity domId) {
-        final RelationAnalysis.Knowledge k1 = ra.getKnowledge(domId.getOperand());
-        Map<Event, Set<Event>> out = k1.getMaySet().getOutMap();
-        MutableEventGraph result = new MapEventGraph();
-        news.apply((e1, e2) ->
-            out.getOrDefault(e1, Set.of()).forEach(e -> {
-                if (!k1.getMustSet().contains(e1, e)) {
-                    result.add(e1, e);
+    public Map<Relation, EventGraph> visitProjection(Projection projection) {
+        final MutableEventGraph result = new MapEventGraph();
+        final RelationAnalysis.Knowledge k1 = ra.getKnowledge(projection.getOperand());
+        final EventGraph mayGraph = k1.getMaySet();
+        final EventGraph mustGraph = k1.getMustSet();
+        final boolean dom = projection.getDimension() == Projection.Dimension.DOMAIN;
+        final Map<Event, Set<Event>> altMap = dom ? mayGraph.getOutMap() : mayGraph.getInMap();
+        news.apply((e1, e2) -> {
+            assert e1.equals(e2);
+            for (Event alt : altMap.getOrDefault(e1, Set.of())) {
+                if (!mustGraph.contains(dom ? e1 : alt, dom ? alt : e1)) {
+                    result.add(dom ? e1 : alt, dom ? alt : e1);
                 }
-            })
-        );
-        return Map.of(domId.getOperand(), result);
+            }
+        });
+        return Map.of(projection.getOperand(), result);
     }
 
     @Override
-    public Map<Relation, EventGraph> visitRangeIdentity(RangeIdentity rangeId) {
-        final RelationAnalysis.Knowledge k1 = ra.getKnowledge(rangeId.getOperand());
-        Map<Event, Set<Event>> in = k1.getMaySet().getInMap();
-        MutableEventGraph result = new MapEventGraph();
-        news.apply((e1, e2) ->
-            in.getOrDefault(e2, Set.of()).forEach(e -> {
-                if (!k1.getMustSet().contains(e, e2)) {
-                    result.add(e, e2);
-                }
-            })
-        );
-        return Map.of(rangeId.getOperand(), result);
+    public Map<Relation, EventGraph> visitSetIdentity(SetIdentity id) {
+        return Map.of(id.getDomain(), filterUnknowns(news, id.getDomain()));
     }
 
     @Override
     public Map<Relation, EventGraph> visitInverse(Inverse inv) {
-        final RelationAnalysis.Knowledge k1 = ra.getKnowledge(inv.getOperand());
-        return Map.of(inv.getOperand(),
-                news.inverse().filter((e1, e2) -> k1.getMaySet().contains(e1, e2) && !k1.getMustSet().contains(e1, e2)));
+        return Map.of(inv.getOperand(), filterUnknowns(news.inverse(), inv.getOperand()));
+    }
+
+    @Override
+    public Map<Relation, EventGraph> visitProduct(CartesianProduct product) {
+        final RelationAnalysis.Knowledge k1 = ra.getKnowledge(product.getDomain());
+        final RelationAnalysis.Knowledge k2 = ra.getKnowledge(product.getRange());
+        final MutableEventGraph set1 = new MapEventGraph();
+        final MutableEventGraph set2 = new MapEventGraph();
+        for (Event e1 : news.getDomain()) {
+            if (k1.getMaySet().contains(e1, e1) && !k1.getMustSet().contains(e1, e1)) {
+                set1.add(e1, e1);
+            }
+            for (Event e2 : news.getRange(e1)) {
+                if (k2.getMaySet().contains(e2, e2) && !k2.getMustSet().contains(e2, e2)) {
+                    set2.add(e2, e2);
+                }
+            }
+        }
+        return Map.of(product.getDomain(), set1, product.getRange(), set2);
     }
 
     @Override

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/encoding/IREvaluator.java

@@ -112,7 +112,17 @@ public TypedValue<IntegerType, BigInteger> size(MemoryObject memoryObject) {
     // ====================================================================================
     // Memory Model
 
+    public boolean hasElement(Relation rel, Event a) {
+        Preconditions.checkArgument(rel.isSet(), "Non-unary relation %s", rel);
+        return TRUE.equals(smtModel.evaluate(ctx.edge(rel, a, a)));
+    }
+
+    public boolean hasElement(EncodingContext.EdgeEncoder edgeEncoder, Event a) {
+        return TRUE.equals(smtModel.evaluate(edgeEncoder.encode(a, a)));
+    }
+
     public boolean hasEdge(Relation rel, Event a, Event b) {
+        Preconditions.checkArgument(rel.isRelation(), "Non-binary relation %s", rel);
         return TRUE.equals(smtModel.evaluate(ctx.edge(rel, a, b)));
     }
 

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

@@ -46,16 +46,6 @@ public Boolean visitFree(Free definition) {
         return doUpdateSelf(definition);
     }
 
-    @Override
-    public Boolean visitProduct(CartesianProduct definition) {
-        return doUpdateSelf(definition);
-    }
-
-    @Override
-    public Boolean visitSetIdentity(SetIdentity definition) {
-        return doUpdateSelf(definition);
-    }
-
     @Override
     public Boolean visitExternal(External definition) {
         return doUpdateSelf(definition);
@@ -152,27 +142,50 @@ public Boolean visitSyncWith(SyncWith definition) {
     }
 
     @Override
-    public Boolean visitDomainIdentity(DomainIdentity definition) {
+    public Boolean visitProduct(CartesianProduct definition) {
         if (doUpdateSelf(definition)) {
             long start = System.currentTimeMillis();
-            MutableEventGraph operandUpdate = new MapEventGraph();
-            Map<Event, Set<Event>> outMap = ra.getKnowledge(definition.getOperand()).getMaySet().getOutMap();
-            update.getDomain().forEach(e1 -> operandUpdate.addRange(e1, outMap.get(e1)));
-            setUpdate(operandUpdate);
+            MutableEventGraph domainUpdate = new MapEventGraph();
+            MutableEventGraph rangeUpdate = new MapEventGraph();
+            update.getDomain().forEach(e1 -> domainUpdate.add(e1, e1));
+            update.getRange().forEach(e2 -> rangeUpdate.add(e2, e2));
             operandTime(definition, start, System.currentTimeMillis());
-            definition.getOperand().getDefinition().accept(this);
+            setUpdate(domainUpdate);
+            definition.getDomain().getDefinition().accept(this);
+            setUpdate(rangeUpdate);
+            definition.getRange().getDefinition().accept(this);
             return true;
         }
         return false;
     }
 
     @Override
-    public Boolean visitRangeIdentity(RangeIdentity definition) {
+    public Boolean visitSetIdentity(SetIdentity definition) {
         if (doUpdateSelf(definition)) {
             long start = System.currentTimeMillis();
-            MutableEventGraph operandUpdate = new MapEventGraph();
-            Map<Event, Set<Event>> inMap = ra.getKnowledge(definition.getOperand()).getMaySet().getInMap();
-            update.getDomain().forEach(e2 -> inMap.get(e2).forEach(e1 -> operandUpdate.add(e1, e2)));
+            MutableEventGraph domainUpdate = new MapEventGraph();
+            update.apply((e1, e2) -> domainUpdate.add(e1, e1));
+            operandTime(definition, start, System.currentTimeMillis());
+            setUpdate(domainUpdate);
+            definition.getDomain().getDefinition().accept(this);
+            return true;
+        }
+        return false;
+    }
+
+    @Override
+    public Boolean visitProjection(Projection definition) {
+        if (doUpdateSelf(definition)) {
+            final long start = System.currentTimeMillis();
+            final MutableEventGraph operandUpdate = new MapEventGraph();
+            final boolean dom = definition.getDimension() == Projection.Dimension.DOMAIN;
+            final EventGraph maySet = ra.getKnowledge(definition.getOperand()).getMaySet();
+            final Map<Event, Set<Event>> altMap = dom ? maySet.getOutMap() : maySet.getInMap();
+            if (dom) {
+                update.getDomain().forEach(e1 -> operandUpdate.addRange(e1, altMap.get(e1)));
+            } else {
+                update.getDomain().forEach(e2 -> altMap.get(e2).forEach(e1 -> operandUpdate.add(e1, e2)));
+            }
             setUpdate(operandUpdate);
             operandTime(definition, start, System.currentTimeMillis());
             definition.getOperand().getDefinition().accept(this);

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

@@ -19,6 +19,7 @@
 import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis;
 import com.dat3m.dartagnan.wmm.axiom.Axiom;
 import com.dat3m.dartagnan.wmm.definition.*;
+import com.dat3m.dartagnan.wmm.definition.TagSet;
 import com.dat3m.dartagnan.wmm.utils.Flag;
 import com.dat3m.dartagnan.wmm.utils.graph.EventGraph;
 import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph;
@@ -235,9 +236,7 @@ private final class RelationEncoder implements Constraint.Visitor<Void> {
                 SyncWith.class,
                 SameVirtualLocation.class, // FIXME?!
                 Empty.class,
-                // Static because the underlying sets are static:
-                SetIdentity.class,
-                CartesianProduct.class
+                TagSet.class
         ));
 
         final Program program = context.getTask().getProgram();
@@ -378,37 +377,21 @@ public Void visitComposition(Composition comp) {
         }
 
         @Override
-        public Void visitDomainIdentity(DomainIdentity domId) {
-            final Relation rel = domId.getDefinedRelation();
-            final Relation r1 = domId.getOperand();
-            Map<Event, Set<Event>> mayOut = ra.getKnowledge(r1).getMaySet().getOutMap();
-            EncodingContext.EdgeEncoder enc0 = context.edge(rel);
-            EncodingContext.EdgeEncoder enc1 = context.edge(r1);
+        public Void visitProjection(Projection projection) {
+            final Relation rel = projection.getDefinedRelation();
+            final Relation r1 = projection.getOperand();
+            final EncodingContext.EdgeEncoder enc0 = context.edge(rel);
+            final EncodingContext.EdgeEncoder enc1 = context.edge(r1);
+            final boolean dom = projection.getDimension() == Projection.Dimension.DOMAIN;
+            final EventGraph may1 = ra.getKnowledge(r1).getMaySet();
+            final Map<Event, Set<Event>> altMap = dom ? may1.getOutMap() : may1.getInMap();
             encodeSets.get(rel).apply((e1, e2) -> {
-                BooleanFormula opt = bmgr.makeFalse();
-                //TODO: Optimize using minSets (but no CAT uses this anyway)
-                for (Event e2Alt : mayOut.getOrDefault(e1, Set.of())) {
-                    opt = bmgr.or(opt, enc1.encode(e1, e2Alt));
+                assert e1.equals(e2);
+                final var opt = new ArrayList<BooleanFormula>();
+                for (Event alt : altMap.getOrDefault(e1, Set.of())) {
+                    opt.add(enc1.encode(dom ? e1 : alt, dom ? alt : e1));
                 }
-                enc.add(bmgr.equivalence(enc0.encode(e1, e2), opt));
-            });
-            return null;
-        }
-
-        @Override
-        public Void visitRangeIdentity(RangeIdentity rangeId) {
-            final Relation rel = rangeId.getDefinedRelation();
-            final Relation r1 = rangeId.getOperand();
-            Map<Event, Set<Event>> mayIn = ra.getKnowledge(r1).getMaySet().getInMap();
-            EncodingContext.EdgeEncoder enc0 = context.edge(rel);
-            EncodingContext.EdgeEncoder enc1 = context.edge(r1);
-            //TODO: Optimize using minSets (but no CAT uses this anyway)
-            encodeSets.get(rel).apply((e1, e2) -> {
-                BooleanFormula opt = bmgr.makeFalse();
-                for (Event e1Alt : mayIn.getOrDefault(e1, Set.of())) {
-                    opt = bmgr.or(opt, enc1.encode(e1Alt, e2));
-                }
-                enc.add(bmgr.equivalence(enc0.encode(e1, e2), opt));
+                enc.add(bmgr.equivalence(enc0.encode(e1, e1), bmgr.or(opt)));
             });
             return null;
         }
@@ -444,6 +427,22 @@ public Void visitTransitiveClosure(TransitiveClosure trans) {
             return null;
         }
 
+        @Override
+        public Void visitSetIdentity(SetIdentity id) {
+            final Relation setId = id.getDefinedRelation();
+            final Relation domain = id.getDomain();
+            EventGraph mustSet = ra.getKnowledge(setId).getMustSet();
+            EncodingContext.EdgeEncoder encSetId = context.edge(setId);
+            EncodingContext.EdgeEncoder encDomain = context.edge(domain);
+            encodeSets.get(setId).apply((e1, e2) ->
+                    enc.add(bmgr.equivalence(
+                            encSetId.encode(e1, e2),
+                            mustSet.contains(e1, e2) ?
+                                    execution(e1, e2) :
+                                    encDomain.encode(e1, e2))));
+            return null;
+        }
+
         @Override
         public Void visitInverse(Inverse inv) {
             final Relation rel = inv.getDefinedRelation();
@@ -460,6 +459,24 @@ public Void visitInverse(Inverse inv) {
             return null;
         }
 
+        @Override
+        public Void visitProduct(CartesianProduct cartesianProduct) {
+            final Relation product = cartesianProduct.getDefinedRelation();
+            final Relation domain = cartesianProduct.getDomain();
+            final Relation range = cartesianProduct.getRange();
+            EventGraph mustSet = ra.getKnowledge(product).getMustSet();
+            EncodingContext.EdgeEncoder encProduct = context.edge(product);
+            EncodingContext.EdgeEncoder encDomain = context.edge(domain);
+            EncodingContext.EdgeEncoder encRange = context.edge(range);
+            encodeSets.get(product).apply((e1, e2) ->
+                    enc.add(bmgr.equivalence(
+                            encProduct.encode(e1, e2),
+                            mustSet.contains(e1, e2) ?
+                                    execution(e1, e2) :
+                                    bmgr.and(encDomain.encode(e1, e1), encRange.encode(e2, e2)))));
+            return null;
+        }
+
         @Override
         public Void visitInternalDataDependency(DirectDataDependency idd) {
             return visitDirectDependency(idd.getDefinedRelation());