Remove term-based relation merging in CAT parser & fix duplicated fre…

…e relations (#632)

* - Removed merging of equivalent relations in cat parser

* - Removed dead code

* Added pass to distinguish different free relations.
This fixes an issue where different free relations accidentally shared the same variables in the encoding.

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

@@ -33,8 +33,6 @@ class VisitorBase extends CatBaseVisitor<Object> {
     private final Map<String, Integer> nameOccurrenceCounter = new HashMap<>();
     // Used to handle recursive definitions properly
     private Relation relationToBeDefined;
-    // Used as optimization to avoid creating multiple relations with (structurally) identical definitions.
-    private final Map<String, Relation> termMap = new HashMap<>();
 
     VisitorBase() {
         this.wmm = new Wmm();
@@ -292,19 +290,7 @@ public Relation visitExprFencerel(ExprFencerelContext ctx) {
     // ============================ Utility ============================
 
     private Relation addDefinition(Definition definition) {
-        Relation definedRelation = definition.getDefinedRelation();
-        String term = definition.getTerm();
-        Relation mappedRelation = termMap.get(definition.getTerm());
-        if (mappedRelation == null) {
-            // This is a new definition.
-            termMap.put(term, definedRelation);
-            return wmm.addDefinition(definition);
-        } else {
-            // We created an already existing definition, so we do not add this definition
-            // to the Wmm and instead delete the relation it is defining (redundantly)
-            wmm.deleteRelation(definedRelation);
-            return mappedRelation;
-        }
+        return wmm.addDefinition(definition);
     }
 
     private void checkNoRecursion(ExpressionContext c) {

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

@@ -0,0 +1,35 @@
+package com.dat3m.dartagnan.wmm.processing;
+
+import com.dat3m.dartagnan.wmm.Relation;
+import com.dat3m.dartagnan.wmm.Wmm;
+import com.dat3m.dartagnan.wmm.definition.Free;
+
+/*
+    This pass makes sure that differently freely defined relations have different names, in particular,
+    unnamed relations will get a dummy name.
+    This makes sure that we generate different encoding variables for different relations
+    (there is no name collision).
+
+    NOTE: We could generalize this pass to give distinguishing names to any pair of different relations
+    if they are unnamed but have the same term. However, this is should only happen to free relations right now.
+ */
+public class MarkFreeRelations implements WmmProcessor {
+
+    private MarkFreeRelations() {
+    }
+
+    public static MarkFreeRelations newInstance() {
+        return new MarkFreeRelations();
+    }
+
+    @Override
+    public void run(Wmm wmm) {
+        int counter = 0;
+        for (Relation rel : wmm.getRelations()) {
+            if (rel.getDefinition() instanceof Free && !rel.hasName()) {
+                wmm.addAlias("free#" + counter, rel);
+                counter++;
+            }
+        }
+    }
+}

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

@@ -118,6 +118,8 @@ private void mergeEquivalentRelations(Wmm wmm, Map<Relation, Relation> eqMap) {
             }
 
             if (c instanceof Definition def && eqMap.get(def.getDefinedRelation()) != def.getDefinedRelation()) {
+                logger.trace("Merging relation {} into relation {}",
+                        def.getDefinedRelation(), eqMap.get(def.getDefinedRelation()));
                 wmm.removeConstraint(c);
             } else if (!(c instanceof Definition.Undefined)) {
                 wmm.removeConstraint(c);
@@ -127,7 +129,6 @@ private void mergeEquivalentRelations(Wmm wmm, Map<Relation, Relation> eqMap) {
 
         eqMap.forEach((r, repr) -> {
             if (r != repr) {
-                logger.debug("Merged relation {} into relation {}", r, repr);
                 wmm.deleteRelation(r);
                 // Transfer names to representative relation.
                 r.getNames().forEach(name -> wmm.addAlias(name, repr));

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

@@ -28,7 +28,8 @@ private WmmProcessingManager(Configuration config) throws InvalidConfigurationEx
         processors.addAll(Arrays.asList(
                 RemoveDeadRelations.newInstance(),
                 MergeEquivalentRelations.newInstance(),
-                FlattenAssociatives.newInstance()
+                FlattenAssociatives.newInstance(),
+                MarkFreeRelations.newInstance()
         ));
         processors.removeIf(Objects::isNull);
     }