Remove Fence class

cat/ppcfences.cat

@@ -1,4 +1,4 @@
-let sync = fencerel(sync)
-let isync = fencerel(isync)
-let lwsync = fencerel(lwsync)
+let sync = po;[sync];po
+let isync = po;[isync];po
+let lwsync = po;[lwsync];po
 let ctrlisync = ctrl & isync

cat/x86fences.cat

@@ -1 +1 @@
-let mfence = fencerel(mfence)
+let mfence = po;[mfence];po

dartagnan/src/main/antlr4/Cat.g4

@@ -51,7 +51,6 @@ expression
     |   LBRAC DOMAIN LPAR e = expression RPAR RBRAC                     # exprDomainIdentity
     |   LBRAC RANGE LPAR e = expression RPAR RBRAC                      # exprRangeIdentity
     |   (TOID LPAR e = expression RPAR | LBRAC e = expression RBRAC)    # exprIdentity
-    |   FENCEREL LPAR e = expression RPAR                               # exprFencerel
     |   LPAR e = expression RPAR                                        # expr
     |   n = NAME                                                        # exprBasic
     |   call = NEW LPAR RPAR                                            # exprNew

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

@@ -356,29 +356,6 @@ public Void visitInverse(Inverse inv) {
             return null;
         }
 
-        @Override
-        public Void visitFences(Fences fence) {
-            final Relation rel = fence.getDefinedRelation();
-            final Filter fenceSet = fence.getFilter();
-            EventGraph mustSet = ra.getKnowledge(rel).getMustSet();
-            List<Event> fences = program.getThreadEvents().stream().filter(fenceSet::apply).toList();
-            EncodingContext.EdgeEncoder encoder = context.edge(rel);
-            encodeSets.get(rel).apply((e1, e2) -> {
-                BooleanFormula orClause;
-                if (mustSet.contains(e1, e2)) {
-                    orClause = bmgr.makeTrue();
-                } else {
-                    orClause = fences.stream()
-                            .filter(f -> e1.getGlobalId() < f.getGlobalId() && f.getGlobalId() < e2.getGlobalId())
-                            .map(context::execution).reduce(bmgr.makeFalse(), bmgr::or);
-                }
-                enc.add(bmgr.equivalence(
-                        encoder.encode(e1, e2),
-                        bmgr.and(execution(e1, e2), orClause)));
-            });
-            return null;
-        }
-
         @Override
         public Void visitInternalDataDependency(DirectDataDependency idd) {
             return visitDirectDependency(idd.getDefinedRelation());

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

@@ -355,14 +355,6 @@ public Relation visitExprCartesian(ExprCartesianContext c) {
         return addDefinition(new CartesianProduct(r0, s1, s2));
     }
 
-    @Override
-    public Relation visitExprFencerel(ExprFencerelContext ctx) {
-        checkNoRecursion(ctx);
-        Relation r0 = wmm.newRelation();
-        Filter s1 = parseAsFilter(ctx.e);
-        return addDefinition(new Fences(r0, s1));
-    }
-
     // ============================ Utility ============================
 
     private Relation addDefinition(Definition definition) {

dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java

@@ -258,8 +258,6 @@ private RelationGraph createGraphFromRelation(Relation rel) {
             graph = new ExternalGraph();
         } else if (relClass == Internal.class) {
             graph = new InternalGraph();
-        } else if (relClass == Fences.class) {
-            throw new UnsupportedOperationException("fencerel is not supported in CAAT.");
         } else if (relClass == SetIdentity.class) {
             SetPredicate set = getOrCreateSetFromFilter(((SetIdentity) rel.getDefinition()).getFilter());
             graph = new SetIdentityGraph(set);

dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java

@@ -514,11 +514,6 @@ private static RefinementModel generateRefinementModel(Wmm original) {
                 if (name.equals(DATA) || name.equals(CTRL) || name.equals(ADDR) || isUnknownDefinitionForCAAT(def)) {
                     constraintsToCut.add(c);
                 }
-            } else if (c instanceof Definition def && def instanceof Fences) {
-                // (iii) continued: fencerel(F) is unsupported in CAAT.
-                //  It should get rewritten to "po;[F];po" by our passes,
-                //  but if it was not, we cut it instead.
-                constraintsToCut.add(c);
             }
         }
 

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java

@@ -70,7 +70,6 @@ default T visitConstraint(Constraint constraint) {
         // These three are semi-derived (they are derived from sets/filters and not from relations).
         default T visitSetIdentity(SetIdentity def) { return visitDefinition(def); }
         default T visitProduct(CartesianProduct def) { return visitDefinition(def); }
-        default T visitFences(Fences fence) { return visitDefinition(fence); }
 
         // Base
         default T visitUndefined(Definition.Undefined def) { return visitDefinition(def); }

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java

@@ -247,10 +247,6 @@ private Definition composition(Relation r0, Relation r1, Relation r2) {
         return new Composition(r0, r1, r2);
     }
 
-    private Definition fence(Relation r0, String name) {
-        return new Fences(r0, Filter.byTag(name));
-    }
-
     private Definition product(Relation r0, String tag1, String tag2) {
         return new CartesianProduct(r0, Filter.byTag(tag1), Filter.byTag(tag2));
     }

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java

@@ -607,39 +607,6 @@ public Knowledge visitInternalDataDependency(DirectDataDependency idd) {
             return computeInternalDependencies(EnumSet.of(DATA, CTRL, OTHER));
         }
 
-        @Override
-        public Knowledge visitFences(Fences fenceDef) {
-            final Filter fence = fenceDef.getFilter();
-            EventGraph may = new EventGraph();
-            EventGraph must = new EventGraph();
-            for (Thread t : program.getThreads()) {
-                List<Event> events = visibleEvents(t);
-                int end = events.size();
-                for (int i = 0; i < end; i++) {
-                    Event f = events.get(i);
-                    if (!fence.apply(f)) {
-                        continue;
-                    }
-                    for (Event x : events.subList(0, i)) {
-                        if (exec.areMutuallyExclusive(x, f)) {
-                            continue;
-                        }
-                        boolean implies = exec.isImplied(x, f);
-                        for (Event y : events.subList(i + 1, end)) {
-                            if (exec.areMutuallyExclusive(x, y) || exec.areMutuallyExclusive(f, y)) {
-                                continue;
-                            }
-                            may.add(x, y);
-                            if (implies || exec.isImplied(y, f)) {
-                                must.add(x, y);
-                            }
-                        }
-                    }
-                }
-            }
-            return new Knowledge(may, must);
-        }
-
         @Override
         public Knowledge visitCASDependency(CASDependency casDep) {
             EventGraph must = new EventGraph();

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/MergeEquivalentRelations.java

@@ -85,9 +85,6 @@ private boolean areEquivalent(Relation r1, Relation r2) {
         if (def1 instanceof CartesianProduct p1 && def2 instanceof CartesianProduct p2) {
             return p1.getFirstFilter().equals(p2.getFirstFilter()) && p1.getSecondFilter().equals(p2.getSecondFilter());
         }
-        if (def1 instanceof Fences f1 && def2 instanceof Fences f2) {
-            return f1.getFilter().equals(f2.getFilter());
-        }
         if (def1 instanceof SameScope s1 && def2 instanceof SameScope s2) {
             return Objects.equals(s1.getSpecificScope(), s2.getSpecificScope());
         }

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessingManager.java

@@ -26,7 +26,6 @@ public class WmmProcessingManager implements WmmProcessor {
     private WmmProcessingManager(Configuration config) throws InvalidConfigurationException {
         config.inject(this);
         processors.addAll(Arrays.asList(
-                NormalizeFenceRelations.newInstance(),
                 AddInitReadHandling.newInstance(),
                 RemoveDeadRelations.newInstance(),
                 MergeEquivalentRelations.newInstance(),

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java

@@ -121,11 +121,6 @@ public CartesianProduct visitProduct(CartesianProduct def) {
         return new CartesianProduct(translate(def.getDefinedRelation()), def.getFirstFilter(), def.getSecondFilter());
     }
 
-    @Override
-    public Fences visitFences(Fences fence) {
-        return new Fences(translate(fence.getDefinedRelation()), fence.getFilter());
-    }
-
     @Override
     public Definition.Undefined visitUndefined(Definition.Undefined def) {
         return new Definition.Undefined(translate(def.getDefinedRelation()));