-
Notifications
You must be signed in to change notification settings - Fork 31
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* - Reworked memory model preprocessing to be similar to program preprocessing. - Added new Wmm pass that merges equivalent relations * - Fixed Property.getSMTVariable to escape variable names. - Fixed ConstraintCopier to preserve axiom names when copying. - Fixed MergeEquivalentRelations to properly distinguish SameScope relations with different scopes. * - Fixed ConstraintCopier failing to copy SameScope properly. - Fixed equality checking between SameScope definitions failing if their scopes were NULL * - Removed MM and MV from RelationNameRepository - Wmm.getOrCreatePredefinedRelation now creates new M*M / M*V relations when needed, relying on MergeEquivalentRelations to merge duplicates later on.
- Loading branch information
1 parent
bf457e3
commit 6cc2789
Showing
15 changed files
with
358 additions
and
114 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
59 changes: 59 additions & 0 deletions
59
dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/FlattenAssociatives.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,59 @@ | ||
| package com.dat3m.dartagnan.wmm.processing; | ||
|
|
||
| import com.dat3m.dartagnan.wmm.Constraint; | ||
| import com.dat3m.dartagnan.wmm.Definition; | ||
| import com.dat3m.dartagnan.wmm.Relation; | ||
| import com.dat3m.dartagnan.wmm.Wmm; | ||
| import com.dat3m.dartagnan.wmm.definition.Intersection; | ||
| import com.dat3m.dartagnan.wmm.definition.Union; | ||
|
|
||
| import java.util.List; | ||
| import java.util.function.BiFunction; | ||
| import java.util.stream.Stream; | ||
|
|
||
| // Flattens nested binary unions/intersections into n-ary ones. | ||
| public class FlattenAssociatives implements WmmProcessor { | ||
|
|
||
| private FlattenAssociatives() { | ||
| } | ||
|
|
||
| public static FlattenAssociatives newInstance() { | ||
| return new FlattenAssociatives(); | ||
| } | ||
|
|
||
| @Override | ||
| public void run(Wmm wmm) { | ||
| flattenAssociatives(wmm, Union.class, Union::new); | ||
| flattenAssociatives(wmm, Intersection.class, Intersection::new); | ||
| } | ||
|
|
||
| private void flattenAssociatives(Wmm wmm, | ||
| Class<? extends Definition> cls, | ||
| BiFunction<Relation, Relation[], Definition> constructor | ||
| ) { | ||
| final List<Relation> relations = List.copyOf(wmm.getRelations()); | ||
| final List<Constraint> constraints = wmm.getConstraints().stream() | ||
| .filter(c -> !(c instanceof Definition)).toList(); | ||
|
|
||
| for (Relation r : relations) { | ||
| if (r.hasName() || !cls.isInstance(r.getDefinition()) | ||
| || constraints.stream().anyMatch(c -> c.getConstrainedRelations().contains(r))) { | ||
| continue; | ||
| } | ||
| final List<Relation> dependents = relations.stream().filter(x -> x.getDependencies().contains(r)).toList(); | ||
| final Relation p = (dependents.size() == 1 ? dependents.get(0) : null); | ||
| if (p != null && cls.isInstance(p.getDefinition())) { | ||
| final Relation[] o = Stream.of(r, p) | ||
| .flatMap(x -> x.getDependencies().stream()) | ||
| .filter(x -> !r.equals(x)) | ||
| .distinct() | ||
| .toArray(Relation[]::new); | ||
| wmm.removeDefinition(p); | ||
| wmm.addDefinition(constructor.apply(p, o)); | ||
| wmm.removeDefinition(r); | ||
| wmm.deleteRelation(r); | ||
| } | ||
| } | ||
| } | ||
|
|
||
| } |
Oops, something went wrong.