Free relations in CAT (#627)

* - Add "free" relations to CAT * - Centralized handling of the "enableMustSets" option. - Fixed some bugs * Added handling of Free relations to relation merging. * Updated EmptyEventGraphTest
hernanponcedeleon · Feb 28, 2024 · 3c6c580 · 3c6c580
1 parent 6cc2789
commit 3c6c580
Show file tree

Hide file tree

Showing 10 changed files with 130 additions and 86 deletions.
diff --git a/dartagnan/src/main/antlr4/Cat.g4 b/dartagnan/src/main/antlr4/Cat.g4
@@ -49,6 +49,7 @@ expression
     |   FENCEREL LPAR e = expression RPAR                               # exprFencerel
     |   LPAR e = expression RPAR                                        # expr
     |   n = NAME                                                        # exprBasic
+    |   call = NEW LPAR RPAR                                            # exprNew
     ;
 
 LET     :   'let';
@@ -81,6 +82,7 @@ RBRAC   :   ']';
 FENCEREL    :   'fencerel';
 DOMAIN      :   'domain';
 RANGE       :   'range';
+NEW         :   'new';
 
 FLAG       :   'flag';
 

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java
@@ -153,6 +153,14 @@ public Void visitDefinition(Definition def) {
             return null;
         }
 
+        @Override
+        public Void visitFree(Free def) {
+            final Relation rel = def.getDefinedRelation();
+            EncodingContext.EdgeEncoder edge = context.edge(rel);
+            encodeSets.get(rel).apply((e1, e2) -> enc.add(bmgr.implication(edge.encode(e1, e2), execution(e1, e2))));
+            return null;
+        }
+
         @Override
         public Void visitUnion(Union union) {
             final Relation rel = union.getDefinedRelation();

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java
@@ -143,6 +143,11 @@ public Object visitExpr(ExprContext ctx) {
         return ctx.e.accept(this);
     }
 
+    @Override
+    public Object visitExprNew(ExprNewContext ctx) {
+        return addDefinition(new Free(wmm.newRelation()));
+    }
+
     @Override
     public Object visitExprBasic(ExprBasicContext ctx) {
         String name = ctx.n.getText();

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java
@@ -90,6 +90,7 @@ default T visitConstraint(Constraint constraint) {
 
         // Base
         default T visitUndefined(Definition.Undefined def) { return visitDefinition(def); }
+        default T visitFree(Free def) { return visitDefinition(def); }
         default T visitEmpty(Empty def) { return visitDefinition(def); }
         default T visitProgramOrder(ProgramOrder po) { return visitDefinition(po); }
         default T visitExternal(External ext) { return visitDefinition(ext); }