Skip to content

Commit aafa016

Browse files
xerenxeren
authored
Support unary predicates in cat (#908)
1 parent 24a65b2 commit aafa016

File tree

68 files changed

+1025
-640
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

68 files changed

+1025
-640
lines changed

‎dartagnan/src/main/antlr4/Cat.g4‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -48,12 +48,13 @@ expression
4848
| e1 = expression BSLASH e2 = expression # exprMinus
4949
| e1 = expression SEMI e2 = expression # exprComposition
5050
| e1 = expression BAR e2 = expression # exprUnion
51-
| LBRAC DOMAIN LPAR e = expression RPAR RBRAC # exprDomainIdentity
52-
| LBRAC RANGE LPAR e = expression RPAR RBRAC # exprRangeIdentity
51+
| DOMAIN LPAR e = expression RPAR # exprDomain
52+
| RANGE LPAR e = expression RPAR # exprRange
5353
| (TOID LPAR e = expression RPAR | LBRAC e = expression RBRAC) # exprIdentity
5454
| LPAR e = expression RPAR # expr
5555
| n = NAME # exprBasic
56-
| call = NEW LPAR RPAR # exprNew
56+
| NEW_SET LPAR RPAR # exprNewSet
57+
| NEW_RELATION LPAR RPAR # exprNewRelation
5758
| call = NAME LPAR args = argumentList RPAR # exprCall
5859
;
5960

@@ -103,9 +104,10 @@ LBRAC : '[';
103104
RBRAC : ']';
104105
COMMA : ',';
105106

106-
DOMAIN : 'domain';
107-
RANGE : 'range';
108-
NEW : 'new';
107+
DOMAIN : 'domain';
108+
RANGE : 'range';
109+
NEW_SET : 'newSet';
110+
NEW_RELATION : 'newRelation';
109111

110112
FLAG : 'flag';
111113
UNDEFINED : 'undefined_unless';

‎dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java‎

Lines changed: 37 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -84,40 +84,51 @@ public Map<Relation, EventGraph> visitComposition(Composition comp) {
8484
}
8585

8686
@Override
87-
public Map<Relation, EventGraph> visitDomainIdentity(DomainIdentity domId) {
88-
final RelationAnalysis.Knowledge k1 = ra.getKnowledge(domId.getOperand());
89-
Map<Event, Set<Event>> out = k1.getMaySet().getOutMap();
90-
MutableEventGraph result = new MapEventGraph();
91-
news.apply((e1, e2) ->
92-
out.getOrDefault(e1, Set.of()).forEach(e -> {
93-
if (!k1.getMustSet().contains(e1, e)) {
94-
result.add(e1, e);
87+
public Map<Relation, EventGraph> visitProjection(Projection projection) {
88+
final MutableEventGraph result = new MapEventGraph();
89+
final RelationAnalysis.Knowledge k1 = ra.getKnowledge(projection.getOperand());
90+
final EventGraph mayGraph = k1.getMaySet();
91+
final EventGraph mustGraph = k1.getMustSet();
92+
final boolean dom = projection.getDimension() == Projection.Dimension.DOMAIN;
93+
final Map<Event, Set<Event>> altMap = dom ? mayGraph.getOutMap() : mayGraph.getInMap();
94+
news.apply((e1, e2) -> {
95+
assert e1.equals(e2);
96+
for (Event alt : altMap.getOrDefault(e1, Set.of())) {
97+
if (!mustGraph.contains(dom ? e1 : alt, dom ? alt : e1)) {
98+
result.add(dom ? e1 : alt, dom ? alt : e1);
9599
}
96-
})
97-
);
98-
return Map.of(domId.getOperand(), result);
100+
}
101+
});
102+
return Map.of(projection.getOperand(), result);
99103
}
100104

101105
@Override
102-
public Map<Relation, EventGraph> visitRangeIdentity(RangeIdentity rangeId) {
103-
final RelationAnalysis.Knowledge k1 = ra.getKnowledge(rangeId.getOperand());
104-
Map<Event, Set<Event>> in = k1.getMaySet().getInMap();
105-
MutableEventGraph result = new MapEventGraph();
106-
news.apply((e1, e2) ->
107-
in.getOrDefault(e2, Set.of()).forEach(e -> {
108-
if (!k1.getMustSet().contains(e, e2)) {
109-
result.add(e, e2);
110-
}
111-
})
112-
);
113-
return Map.of(rangeId.getOperand(), result);
106+
public Map<Relation, EventGraph> visitSetIdentity(SetIdentity id) {
107+
return Map.of(id.getDomain(), filterUnknowns(news, id.getDomain()));
114108
}
115109

116110
@Override
117111
public Map<Relation, EventGraph> visitInverse(Inverse inv) {
118-
final RelationAnalysis.Knowledge k1 = ra.getKnowledge(inv.getOperand());
119-
return Map.of(inv.getOperand(),
120-
news.inverse().filter((e1, e2) -> k1.getMaySet().contains(e1, e2) && !k1.getMustSet().contains(e1, e2)));
112+
return Map.of(inv.getOperand(), filterUnknowns(news.inverse(), inv.getOperand()));
113+
}
114+
115+
@Override
116+
public Map<Relation, EventGraph> visitProduct(CartesianProduct product) {
117+
final RelationAnalysis.Knowledge k1 = ra.getKnowledge(product.getDomain());
118+
final RelationAnalysis.Knowledge k2 = ra.getKnowledge(product.getRange());
119+
final MutableEventGraph set1 = new MapEventGraph();
120+
final MutableEventGraph set2 = new MapEventGraph();
121+
for (Event e1 : news.getDomain()) {
122+
if (k1.getMaySet().contains(e1, e1) && !k1.getMustSet().contains(e1, e1)) {
123+
set1.add(e1, e1);
124+
}
125+
for (Event e2 : news.getRange(e1)) {
126+
if (k2.getMaySet().contains(e2, e2) && !k2.getMustSet().contains(e2, e2)) {
127+
set2.add(e2, e2);
128+
}
129+
}
130+
}
131+
return Map.of(product.getDomain(), set1, product.getRange(), set2);
121132
}
122133

123134
@Override

‎dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -255,6 +255,7 @@ public EdgeEncoder edge(Relation relation) {
255255
EventGraph must = k.getMustSet();
256256
EdgeEncoder variable = relation.getDefinition().getEdgeVariableEncoder(this);
257257
return (e1, e2) -> {
258+
checkArgument(!relation.isSet() || e1.equals(e2), "Cannot encode pairs of events in an event set");
258259
if (!may.contains(e1, e2)) {
259260
return booleanFormulaManager.makeFalse();
260261
}

‎dartagnan/src/main/java/com/dat3m/dartagnan/encoding/IREvaluator.java‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,17 @@ public TypedValue<IntegerType, BigInteger> size(MemoryObject memoryObject) {
112112
// ====================================================================================
113113
// Memory Model
114114

115+
public boolean hasElement(Relation rel, Event a) {
116+
Preconditions.checkArgument(rel.isSet(), "Non-unary relation %s", rel);
117+
return TRUE.equals(smtModel.evaluate(ctx.edge(rel, a, a)));
118+
}
119+
120+
public boolean hasElement(EncodingContext.EdgeEncoder edgeEncoder, Event a) {
121+
return TRUE.equals(smtModel.evaluate(edgeEncoder.encode(a, a)));
122+
}
123+
115124
public boolean hasEdge(Relation rel, Event a, Event b) {
125+
Preconditions.checkArgument(rel.isRelation(), "Non-binary relation %s", rel);
116126
return TRUE.equals(smtModel.evaluate(ctx.edge(rel, a, b)));
117127
}
118128

‎dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java‎

Lines changed: 33 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -46,16 +46,6 @@ public Boolean visitFree(Free definition) {
4646
return doUpdateSelf(definition);
4747
}
4848

49-
@Override
50-
public Boolean visitProduct(CartesianProduct definition) {
51-
return doUpdateSelf(definition);
52-
}
53-
54-
@Override
55-
public Boolean visitSetIdentity(SetIdentity definition) {
56-
return doUpdateSelf(definition);
57-
}
58-
5949
@Override
6050
public Boolean visitExternal(External definition) {
6151
return doUpdateSelf(definition);
@@ -152,27 +142,50 @@ public Boolean visitSyncWith(SyncWith definition) {
152142
}
153143

154144
@Override
155-
public Boolean visitDomainIdentity(DomainIdentity definition) {
145+
public Boolean visitProduct(CartesianProduct definition) {
156146
if (doUpdateSelf(definition)) {
157147
long start = System.currentTimeMillis();
158-
MutableEventGraph operandUpdate = new MapEventGraph();
159-
Map<Event, Set<Event>> outMap = ra.getKnowledge(definition.getOperand()).getMaySet().getOutMap();
160-
update.getDomain().forEach(e1 -> operandUpdate.addRange(e1, outMap.get(e1)));
161-
setUpdate(operandUpdate);
148+
MutableEventGraph domainUpdate = new MapEventGraph();
149+
MutableEventGraph rangeUpdate = new MapEventGraph();
150+
update.getDomain().forEach(e1 -> domainUpdate.add(e1, e1));
151+
update.getRange().forEach(e2 -> rangeUpdate.add(e2, e2));
162152
operandTime(definition, start, System.currentTimeMillis());
163-
definition.getOperand().getDefinition().accept(this);
153+
setUpdate(domainUpdate);
154+
definition.getDomain().getDefinition().accept(this);
155+
setUpdate(rangeUpdate);
156+
definition.getRange().getDefinition().accept(this);
164157
return true;
165158
}
166159
return false;
167160
}
168161

169162
@Override
170-
public Boolean visitRangeIdentity(RangeIdentity definition) {
163+
public Boolean visitSetIdentity(SetIdentity definition) {
171164
if (doUpdateSelf(definition)) {
172165
long start = System.currentTimeMillis();
173-
MutableEventGraph operandUpdate = new MapEventGraph();
174-
Map<Event, Set<Event>> inMap = ra.getKnowledge(definition.getOperand()).getMaySet().getInMap();
175-
update.getDomain().forEach(e2 -> inMap.get(e2).forEach(e1 -> operandUpdate.add(e1, e2)));
166+
MutableEventGraph domainUpdate = new MapEventGraph();
167+
update.apply((e1, e2) -> domainUpdate.add(e1, e1));
168+
operandTime(definition, start, System.currentTimeMillis());
169+
setUpdate(domainUpdate);
170+
definition.getDomain().getDefinition().accept(this);
171+
return true;
172+
}
173+
return false;
174+
}
175+
176+
@Override
177+
public Boolean visitProjection(Projection definition) {
178+
if (doUpdateSelf(definition)) {
179+
final long start = System.currentTimeMillis();
180+
final MutableEventGraph operandUpdate = new MapEventGraph();
181+
final boolean dom = definition.getDimension() == Projection.Dimension.DOMAIN;
182+
final EventGraph maySet = ra.getKnowledge(definition.getOperand()).getMaySet();
183+
final Map<Event, Set<Event>> altMap = dom ? maySet.getOutMap() : maySet.getInMap();
184+
if (dom) {
185+
update.getDomain().forEach(e1 -> operandUpdate.addRange(e1, altMap.get(e1)));
186+
} else {
187+
update.getDomain().forEach(e2 -> altMap.get(e2).forEach(e1 -> operandUpdate.add(e1, e2)));
188+
}
176189
setUpdate(operandUpdate);
177190
operandTime(definition, start, System.currentTimeMillis());
178191
definition.getOperand().getDefinition().accept(this);

‎dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java‎

Lines changed: 49 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@
1919
import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis;
2020
import com.dat3m.dartagnan.wmm.axiom.Axiom;
2121
import com.dat3m.dartagnan.wmm.definition.*;
22+
import com.dat3m.dartagnan.wmm.definition.TagSet;
2223
import com.dat3m.dartagnan.wmm.utils.Flag;
2324
import com.dat3m.dartagnan.wmm.utils.graph.EventGraph;
2425
import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph;
@@ -235,9 +236,7 @@ private final class RelationEncoder implements Constraint.Visitor<Void> {
235236
SyncWith.class,
236237
SameVirtualLocation.class, // FIXME?!
237238
Empty.class,
238-
// Static because the underlying sets are static:
239-
SetIdentity.class,
240-
CartesianProduct.class
239+
TagSet.class
241240
));
242241

243242
final Program program = context.getTask().getProgram();
@@ -378,37 +377,21 @@ public Void visitComposition(Composition comp) {
378377
}
379378

380379
@Override
381-
public Void visitDomainIdentity(DomainIdentity domId) {
382-
final Relation rel = domId.getDefinedRelation();
383-
final Relation r1 = domId.getOperand();
384-
Map<Event, Set<Event>> mayOut = ra.getKnowledge(r1).getMaySet().getOutMap();
385-
EncodingContext.EdgeEncoder enc0 = context.edge(rel);
386-
EncodingContext.EdgeEncoder enc1 = context.edge(r1);
380+
public Void visitProjection(Projection projection) {
381+
final Relation rel = projection.getDefinedRelation();
382+
final Relation r1 = projection.getOperand();
383+
final EncodingContext.EdgeEncoder enc0 = context.edge(rel);
384+
final EncodingContext.EdgeEncoder enc1 = context.edge(r1);
385+
final boolean dom = projection.getDimension() == Projection.Dimension.DOMAIN;
386+
final EventGraph may1 = ra.getKnowledge(r1).getMaySet();
387+
final Map<Event, Set<Event>> altMap = dom ? may1.getOutMap() : may1.getInMap();
387388
encodeSets.get(rel).apply((e1, e2) -> {
388-
BooleanFormula opt = bmgr.makeFalse();
389-
//TODO: Optimize using minSets (but no CAT uses this anyway)
390-
for (Event e2Alt : mayOut.getOrDefault(e1, Set.of())) {
391-
opt = bmgr.or(opt, enc1.encode(e1, e2Alt));
389+
assert e1.equals(e2);
390+
final var opt = new ArrayList<BooleanFormula>();
391+
for (Event alt : altMap.getOrDefault(e1, Set.of())) {
392+
opt.add(enc1.encode(dom ? e1 : alt, dom ? alt : e1));
392393
}
393-
enc.add(bmgr.equivalence(enc0.encode(e1, e2), opt));
394-
});
395-
return null;
396-
}
397-
398-
@Override
399-
public Void visitRangeIdentity(RangeIdentity rangeId) {
400-
final Relation rel = rangeId.getDefinedRelation();
401-
final Relation r1 = rangeId.getOperand();
402-
Map<Event, Set<Event>> mayIn = ra.getKnowledge(r1).getMaySet().getInMap();
403-
EncodingContext.EdgeEncoder enc0 = context.edge(rel);
404-
EncodingContext.EdgeEncoder enc1 = context.edge(r1);
405-
//TODO: Optimize using minSets (but no CAT uses this anyway)
406-
encodeSets.get(rel).apply((e1, e2) -> {
407-
BooleanFormula opt = bmgr.makeFalse();
408-
for (Event e1Alt : mayIn.getOrDefault(e1, Set.of())) {
409-
opt = bmgr.or(opt, enc1.encode(e1Alt, e2));
410-
}
411-
enc.add(bmgr.equivalence(enc0.encode(e1, e2), opt));
394+
enc.add(bmgr.equivalence(enc0.encode(e1, e1), bmgr.or(opt)));
412395
});
413396
return null;
414397
}
@@ -444,6 +427,22 @@ public Void visitTransitiveClosure(TransitiveClosure trans) {
444427
return null;
445428
}
446429

430+
@Override
431+
public Void visitSetIdentity(SetIdentity id) {
432+
final Relation setId = id.getDefinedRelation();
433+
final Relation domain = id.getDomain();
434+
EventGraph mustSet = ra.getKnowledge(setId).getMustSet();
435+
EncodingContext.EdgeEncoder encSetId = context.edge(setId);
436+
EncodingContext.EdgeEncoder encDomain = context.edge(domain);
437+
encodeSets.get(setId).apply((e1, e2) ->
438+
enc.add(bmgr.equivalence(
439+
encSetId.encode(e1, e2),
440+
mustSet.contains(e1, e2) ?
441+
execution(e1, e2) :
442+
encDomain.encode(e1, e2))));
443+
return null;
444+
}
445+
447446
@Override
448447
public Void visitInverse(Inverse inv) {
449448
final Relation rel = inv.getDefinedRelation();
@@ -460,6 +459,24 @@ public Void visitInverse(Inverse inv) {
460459
return null;
461460
}
462461

462+
@Override
463+
public Void visitProduct(CartesianProduct cartesianProduct) {
464+
final Relation product = cartesianProduct.getDefinedRelation();
465+
final Relation domain = cartesianProduct.getDomain();
466+
final Relation range = cartesianProduct.getRange();
467+
EventGraph mustSet = ra.getKnowledge(product).getMustSet();
468+
EncodingContext.EdgeEncoder encProduct = context.edge(product);
469+
EncodingContext.EdgeEncoder encDomain = context.edge(domain);
470+
EncodingContext.EdgeEncoder encRange = context.edge(range);
471+
encodeSets.get(product).apply((e1, e2) ->
472+
enc.add(bmgr.equivalence(
473+
encProduct.encode(e1, e2),
474+
mustSet.contains(e1, e2) ?
475+
execution(e1, e2) :
476+
bmgr.and(encDomain.encode(e1, e1), encRange.encode(e2, e2)))));
477+
return null;
478+
}
479+
463480
@Override
464481
public Void visitInternalDataDependency(DirectDataDependency idd) {
465482
return visitDirectDependency(idd.getDefinedRelation());

0 commit comments

Comments
 (0)