Skip to content

Commit

Permalink
Remove term-based relation merging in CAT parser & fix duplicated fre…
Browse files Browse the repository at this point in the history
…e relations (hernanponcedeleon#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.
  • Loading branch information
ThomasHaas authored Mar 6, 2024
1 parent 9f8b630 commit b9653ff
Show file tree
Hide file tree
Showing 4 changed files with 40 additions and 17 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -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) {
Expand Down
Original file line number Diff line number Diff line change
@@ -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++;
}
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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));
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand Down

0 comments on commit b9653ff

Please sign in to comment.