Skip to content

Commit

Permalink
Add support for recursive relations
Browse files Browse the repository at this point in the history
  • Loading branch information
Dmitry Ivanov committed Aug 8, 2024
1 parent 2c678be commit 812088a
Showing 1 changed file with 74 additions and 6 deletions.
80 changes: 74 additions & 6 deletions dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/DatalogRelationAnalysis.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -374,17 +374,17 @@ public EventGraph findTransitivelyImpliedCo(Relation co) {
}

private String getRelationDatalogName(Relation r) {
String name = relationToDatalogName.computeIfAbsent(r, k -> sanitize(r.getDefinition().accept(new DatalogNameVisitor()).toString()));
return name.length() < 200 ? name : "rel" + System.identityHashCode(name);
return getRelationDatalogName(r, false);
}

public String getRelationDatalogName(Relation r, boolean full) {
String name = relationToDatalogName.computeIfAbsent(r, k -> sanitize(r.getDefinition().accept(new DatalogNameVisitor()).toString()));
return full || name.length() < 200 ? name : "rel" + System.identityHashCode(name);
String name = relationToDatalogName.computeIfAbsent(r, k -> sanitize(r.getDefinition().accept(new DatalogNameVisitor(r)).toString()));
return full || name.length() < 200 ? name : "rel" + System.identityHashCode(r);
}

private String getFilterDatalogName(Filter f) {
return filterToDatalogName.computeIfAbsent(f, k -> sanitize(f.accept(new DatalogNameVisitor()).toString()));
String name = filterToDatalogName.computeIfAbsent(f, k -> sanitize(f.accept(new DatalogNameVisitor(f)).toString()));
return name.length() < 200 ? name : "fil" + System.identityHashCode(f);
}

@FunctionalInterface
Expand Down Expand Up @@ -548,17 +548,46 @@ public void run() {

private String sanitize(String s) {
assert (s != null);
String result = VISIBLE.equals(s) ? "VISIBLE" : s.replace('-', '_').replace("__", "_VISIBLE");
String result = VISIBLE.equals(s) ? "VISIBLE" : s.replaceAll("[\\-.]", "_").replace("__", "_VISIBLE");
sanitizedToOriginalName.putIfAbsent(result, s);
return result;
}

private class DatalogNameVisitor implements Definition.Visitor<StringBuilder>, Filter.Visitor<StringBuilder> {

private final StringBuilder name = new StringBuilder();
private final Object target;
private boolean recursive = false;
private String recursiveName = null;

public DatalogNameVisitor(Filter filter) {
target = filter;
}

public DatalogNameVisitor(Relation relation) {
target = relation;
}

private boolean checkRecursion(Object target) {
if (!Objects.equals(this.target, target)) {
return false;
}
if (!recursive) {
recursive = true;
return false;
}
if (recursiveName == null) {
recursiveName = "name" + System.identityHashCode(this.target);
name.insert(0, "recursive_" + recursiveName);
}
return true;
}

@Override
public StringBuilder visitUnion(Union def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
}
verify(!def.getOperands().isEmpty());
name.append("union_".repeat(def.getOperands().size() - 1));
name.setLength(name.length() - 1);
Expand All @@ -571,6 +600,9 @@ public StringBuilder visitUnion(Union def) {

@Override
public StringBuilder visitIntersection(Intersection def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
}
verify(!def.getOperands().isEmpty());
name.append("intersection_".repeat(def.getOperands().size() - 1));
name.setLength(name.length() - 1);
Expand All @@ -583,6 +615,9 @@ public StringBuilder visitIntersection(Intersection def) {

@Override
public StringBuilder visitDifference(Difference def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
}
name.append("difference");
Stream.of(def.getMinuend(), def.getSubtrahend()).map(Relation::getDefinition).forEachOrdered(d -> {
name.append("_");
Expand All @@ -593,6 +628,9 @@ public StringBuilder visitDifference(Difference def) {

@Override
public StringBuilder visitComposition(Composition def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
}
name.append("composition");
Stream.of(def.getLeftOperand(), def.getRightOperand()).map(Relation::getDefinition).forEachOrdered(d -> {
name.append("_");
Expand All @@ -603,36 +641,54 @@ public StringBuilder visitComposition(Composition def) {

@Override
public StringBuilder visitDomainIdentity(DomainIdentity def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
}
name.append("domain_");
return def.getOperand().getDefinition().accept(this);
}

@Override
public StringBuilder visitRangeIdentity(RangeIdentity def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
}
name.append("identity_range_");
return def.getOperand().getDefinition().accept(this);
}

@Override
public StringBuilder visitInverse(Inverse def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
}
name.append("inverse_");
return def.getOperand().getDefinition().accept(this);
}

@Override
public StringBuilder visitTransitiveClosure(TransitiveClosure def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
}
name.append("closure_");
return def.getOperand().getDefinition().accept(this);
}

@Override
public StringBuilder visitSetIdentity(SetIdentity def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
}
name.append("identity_");
return def.getFilter().accept(this);
}

@Override
public StringBuilder visitProduct(CartesianProduct def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
}
name.append("product_");
def.getFirstFilter().accept(this);
name.append("_");
Expand All @@ -641,6 +697,9 @@ public StringBuilder visitProduct(CartesianProduct def) {

@Override
public StringBuilder visitFences(Fences fence) {
if (checkRecursion(fence.getDefinedRelation())) {
return name.append(recursiveName);
}
name.append("fence_");
return fence.getFilter().accept(this);
}
Expand Down Expand Up @@ -747,6 +806,9 @@ public StringBuilder visitTagFilter(TagFilter tagFilter) {

@Override
public StringBuilder visitIntersectionFilter(IntersectionFilter intersectionFilter) {
if (checkRecursion(intersectionFilter)) {
return name.append(recursiveName);
}
name.append("intersection");
Stream.of(intersectionFilter.getLeft(), intersectionFilter.getRight()).forEachOrdered(f -> {
name.append("_");
Expand All @@ -757,6 +819,9 @@ public StringBuilder visitIntersectionFilter(IntersectionFilter intersectionFilt

@Override
public StringBuilder visitDifferenceFilter(DifferenceFilter differenceFilter) {
if (checkRecursion(differenceFilter)) {
return name.append(recursiveName);
}
name.append("difference");
Stream.of(differenceFilter.getLeft(), differenceFilter.getRight()).forEachOrdered(f -> {
name.append("_");
Expand All @@ -767,6 +832,9 @@ public StringBuilder visitDifferenceFilter(DifferenceFilter differenceFilter) {

@Override
public StringBuilder visitUnionFilter(UnionFilter unionFilter) {
if (checkRecursion(unionFilter)) {
return name.append(recursiveName);
}
name.append("union");
Stream.of(unionFilter.getLeft(), unionFilter.getRight()).forEachOrdered(f -> {
name.append("_");
Expand Down

0 comments on commit 812088a

Please sign in to comment.