Skip to content

Commit ffc1278

Browse files
xerenhernanponcedeleon
authored andcommitted
Refactor
1 parent 34b262f commit ffc1278

35 files changed

+62
-62
lines changed

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

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

115115
public boolean hasElement(Relation rel, Event a) {
116-
Preconditions.checkArgument(rel.isUnaryRelation(), "Non-unary relation %s", rel);
116+
Preconditions.checkArgument(rel.isSet(), "Non-unary relation %s", rel);
117117
return TRUE.equals(smtModel.evaluate(ctx.edge(rel, a, a)));
118118
}
119119

@@ -122,7 +122,7 @@ public boolean hasElement(EncodingContext.EdgeEncoder edgeEncoder, Event a) {
122122
}
123123

124124
public boolean hasEdge(Relation rel, Event a, Event b) {
125-
Preconditions.checkArgument(rel.isBinaryRelation(), "Non-binary relation %s", rel);
125+
Preconditions.checkArgument(rel.isRelation(), "Non-binary relation %s", rel);
126126
return TRUE.equals(smtModel.evaluate(ctx.edge(rel, a, b)));
127127
}
128128

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -283,8 +283,8 @@ public Object visitExprComplement(ExprComplementContext c) {
283283
final Relation visible = wmm.newSet();
284284
wmm.addDefinition(new TagSet(visible, VISIBLE));
285285
final Relation r0 = wmm.newRelation(r1.getArity());
286-
final Relation all = r1.isUnaryRelation() ? visible : wmm.newRelation();
287-
if (!r1.isUnaryRelation()) {
286+
final Relation all = r1.isSet() ? visible : wmm.newRelation();
287+
if (!r1.isSet()) {
288288
wmm.addDefinition(new CartesianProduct(all, visible, visible));
289289
}
290290
return addDefinition(new Difference(r0, all, r1));

dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ private Constraint getOrCreateConstraintFromAxiom(Axiom axiom) {
206206
}
207207

208208
private RelationGraph getOrCreateGraphFromRelation(Relation rel) {
209-
rel.checkBinaryRelation();
209+
rel.checkRelation();
210210
if (predicateToRelationMap.containsKey(rel)) {
211211
return (RelationGraph) predicateToRelationMap.get(rel);
212212
}
@@ -216,7 +216,7 @@ private RelationGraph getOrCreateGraphFromRelation(Relation rel) {
216216
}
217217

218218
private RelationGraph createGraphFromRelation(Relation rel) {
219-
rel.checkBinaryRelation();
219+
rel.checkRelation();
220220
final RelationGraph graph;
221221
final Class<?> relClass = rel.getDefinition().getClass();
222222
final List<Relation> dependencies = rel.getDependencies();
@@ -269,7 +269,7 @@ private RelationGraph createGraphFromRelation(Relation rel) {
269269
}
270270

271271
private SetPredicate getOrCreateSetFromRelation(Relation relation) {
272-
relation.checkUnaryRelation();
272+
relation.checkSet();
273273
final CAATPredicate existing = predicateToRelationMap.get(relation);
274274
if (existing != null) {
275275
return (SetPredicate) existing;

dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ public class DynamicDefaultWMMGraph extends MaterializedWMMGraph {
1212
private final Relation relation;
1313

1414
public DynamicDefaultWMMGraph(Relation rel) {
15-
rel.checkBinaryRelation();
15+
rel.checkRelation();
1616
this.relation = rel;
1717
}
1818

dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ public class DynamicDefaultWMMSet extends MaterializedWMMSet {
1313
private final Relation relation;
1414

1515
public DynamicDefaultWMMSet(Relation rel) {
16-
rel.checkUnaryRelation();
16+
rel.checkSet();
1717
this.relation = rel;
1818
}
1919

dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -242,11 +242,11 @@ private void createModel(Relation r) {
242242
}
243243

244244
private CAATPredicate createPredicate(Relation r) {
245-
return r.isUnaryRelation() ? createSet(r) : createGraph(r);
245+
return r.isSet() ? createSet(r) : createGraph(r);
246246
}
247247

248248
private SetPredicate createSet(Relation r) {
249-
r.checkUnaryRelation();
249+
r.checkSet();
250250
SetPredicate set = r.getDependencies().isEmpty() ? new SimpleSet() : r.getDefinition().accept(setBuilder);
251251
set.setName(r.getNameOrTerm());
252252
if (!r.isRecursive()) {
@@ -256,7 +256,7 @@ private SetPredicate createSet(Relation r) {
256256
}
257257

258258
private RelationGraph createGraph(Relation r) {
259-
r.checkBinaryRelation();
259+
r.checkRelation();
260260
RelationGraph rg = r.getDependencies().isEmpty() ? new SimpleGraph() : r.getDefinition().accept(graphBuilder);
261261
rg.setName(r.getNameOrTerm());
262262
if (!r.isRecursive()) {
@@ -266,12 +266,12 @@ private RelationGraph createGraph(Relation r) {
266266
}
267267

268268
private SetPredicate getOrCreateSet(Relation r) {
269-
r.checkUnaryRelation();
269+
r.checkSet();
270270
return (SetPredicate) getOrCreatePredicate(r);
271271
}
272272

273273
private RelationGraph getOrCreateGraph(Relation r) {
274-
r.checkBinaryRelation();
274+
r.checkRelation();
275275
return (RelationGraph) getOrCreatePredicate(r);
276276
}
277277

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -43,39 +43,39 @@ public Arity getArity() {
4343
/**
4444
* @return {@code true} if this instance describes an event set in executions. Otherwise {@code false}.
4545
*/
46-
public boolean isUnaryRelation() {
46+
public boolean isSet() {
4747
return arity == Arity.UNARY;
4848
}
4949

5050
/**
5151
* @return {@code true} if this instance describes an event relation in executions. Otherwise {@code false}.
5252
*/
53-
public boolean isBinaryRelation() {
53+
public boolean isRelation() {
5454
return arity == Arity.BINARY;
5555
}
5656

5757
/**
5858
* @throws IllegalArgumentException This instance does not describe an event set in executions.
5959
*/
60-
public void checkUnaryRelation() {
61-
Preconditions.checkArgument(isUnaryRelation(), "Non-unary relation %s.", this);
60+
public void checkSet() {
61+
Preconditions.checkArgument(isSet(), "Non-unary relation %s.", this);
6262
}
6363

6464
/**
6565
* @throws IllegalArgumentException This instance does not describe an event relation in executions.
6666
*/
67-
public void checkBinaryRelation() {
68-
Preconditions.checkArgument(isBinaryRelation(), "Non-binary relation %s.", this);
67+
public void checkRelation() {
68+
Preconditions.checkArgument(isRelation(), "Non-binary relation %s.", this);
6969
}
7070

7171
/**
7272
* @param others Instances of this class.
7373
* @throws IllegalArgumentException At least one instance in {@code others} has a different arity than this.
7474
*/
7575
public void checkEqualArityRelation(Collection<Relation> others) {
76-
Preconditions.checkArgument(!isUnaryRelation() || others.stream().allMatch(Relation::isUnaryRelation),
76+
Preconditions.checkArgument(!isSet() || others.stream().allMatch(Relation::isSet),
7777
"Non-unary relation in %s", others);
78-
Preconditions.checkArgument(!isBinaryRelation() || others.stream().allMatch(Relation::isBinaryRelation),
78+
Preconditions.checkArgument(!isRelation() || others.stream().allMatch(Relation::isRelation),
7979
"Non-binary relation in %s", others);
8080
}
8181

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclicity.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,12 +27,12 @@ public class Acyclicity extends Axiom {
2727

2828
public Acyclicity(Relation rel, boolean negated, boolean flag) {
2929
super(rel, negated, flag);
30-
rel.checkBinaryRelation();
30+
rel.checkRelation();
3131
}
3232

3333
public Acyclicity(Relation rel) {
3434
super(rel, false, false);
35-
rel.checkBinaryRelation();
35+
rel.checkRelation();
3636
}
3737

3838
// Under-approximates the must-set of (rel+ ; rel).

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Irreflexivity.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,12 +16,12 @@ public class Irreflexivity extends Axiom {
1616

1717
public Irreflexivity(Relation rel, boolean negated, boolean flag) {
1818
super(rel, negated, flag);
19-
rel.checkBinaryRelation();
19+
rel.checkRelation();
2020
}
2121

2222
public Irreflexivity(Relation rel) {
2323
super(rel, false, false);
24-
rel.checkBinaryRelation();
24+
rel.checkRelation();
2525
}
2626

2727
@Override

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ public class AMOPairs extends Definition {
88

99
public AMOPairs(Relation r0) {
1010
super(r0, RelationNameRepository.AMO);
11-
r0.checkBinaryRelation();
11+
r0.checkRelation();
1212
}
1313

1414
@Override

0 commit comments

Comments
 (0)