Skip to content

Commit e5d9162

Browse files
rcosta358rcosta358
committed
Renaming
1 parent 0a04e5b commit e5d9162

1 file changed

Lines changed: 35 additions & 35 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java‎

Lines changed: 35 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -29,23 +29,23 @@ public static VCImplication apply(VCImplication implication) {
2929
return apply(implication, List.of());
3030
}
3131

32-
private static VCImplication apply(VCImplication implication, List<Expression> nonZeroTerms) {
32+
private static VCImplication apply(VCImplication implication, List<Expression> nonZeroExpressions) {
3333
if (implication == null)
3434
return null;
3535

3636
Expression expression = implication.getRefinement().getExpression();
37-
Expression simplified = simplify(expression, nonZeroTerms);
37+
Expression simplified = simplify(expression, nonZeroExpressions);
3838
if (!expression.equals(simplified)) {
3939
VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified),
4040
implication.getOrigin());
4141
result.setNext(implication.getNext() == null ? null : implication.getNext().clone());
4242
return result;
4343
}
4444

45-
List<Expression> nextNonZeroTerms = new ArrayList<>(nonZeroTerms);
46-
addNonZeroTerm(implication.getRefinement().getExpression(), nextNonZeroTerms);
45+
List<Expression> nextNoneZeroExpressions = new ArrayList<>(nonZeroExpressions);
46+
addNonZeroExpression(implication.getRefinement().getExpression(), nextNoneZeroExpressions);
4747

48-
VCImplication next = apply(implication.getNext(), nextNonZeroTerms);
48+
VCImplication next = apply(implication.getNext(), nextNoneZeroExpressions);
4949
if (implication.getNext() == null || implication.getNext().equals(next))
5050
return implication;
5151

@@ -57,33 +57,33 @@ private static VCImplication apply(VCImplication implication, List<Expression> n
5757
/**
5858
* Simplifies the first arithmetic identity found inside an expression.
5959
*/
60-
private static Expression simplify(Expression expression, List<Expression> nonZeroTerms) {
60+
private static Expression simplify(Expression expression, List<Expression> nonZeroExpressions) {
6161
if (expression instanceof BinaryExpression binary)
62-
return simplifyBinary(binary, nonZeroTerms);
62+
return simplifyBinary(binary, nonZeroExpressions);
6363
if (expression instanceof UnaryExpression unary)
64-
return simplifyUnary(unary, nonZeroTerms);
64+
return simplifyUnary(unary, nonZeroExpressions);
6565
if (expression instanceof Ite ite)
66-
return simplifyIte(ite, nonZeroTerms);
66+
return simplifyIte(ite, nonZeroExpressions);
6767
if (expression instanceof GroupExpression group)
68-
return simplifyGroup(group, nonZeroTerms);
68+
return simplifyGroup(group, nonZeroExpressions);
6969
return expression.clone();
7070
}
7171

7272
/**
7373
* Simplifies a binary expression by visiting operands before the current node.
7474
*/
75-
private static Expression simplifyBinary(BinaryExpression binary, List<Expression> nonZeroTerms) {
75+
private static Expression simplifyBinary(BinaryExpression binary, List<Expression> nonZeroExpressions) {
7676
Expression left = binary.getFirstOperand();
77-
Expression simplifiedLeft = simplify(left, nonZeroTerms);
77+
Expression simplifiedLeft = simplify(left, nonZeroExpressions);
7878
if (!left.equals(simplifiedLeft))
7979
return new BinaryExpression(simplifiedLeft, binary.getOperator(), binary.getSecondOperand().clone());
8080

8181
Expression right = binary.getSecondOperand();
82-
Expression simplifiedRight = simplify(right, nonZeroTerms);
82+
Expression simplifiedRight = simplify(right, nonZeroExpressions);
8383
if (!right.equals(simplifiedRight))
8484
return new BinaryExpression(left.clone(), binary.getOperator(), simplifiedRight);
8585

86-
Expression simplifiedBinary = simplifyLocalBinary(left, right, binary.getOperator(), nonZeroTerms);
86+
Expression simplifiedBinary = simplifyLocalBinary(left, right, binary.getOperator(), nonZeroExpressions);
8787
if (simplifiedBinary != null)
8888
return simplifiedBinary;
8989

@@ -93,9 +93,9 @@ private static Expression simplifyBinary(BinaryExpression binary, List<Expressio
9393
/**
9494
* Simplifies a unary expression by visiting its operand before the current node.
9595
*/
96-
private static Expression simplifyUnary(UnaryExpression unary, List<Expression> nonZeroTerms) {
96+
private static Expression simplifyUnary(UnaryExpression unary, List<Expression> nonZeroExpressions) {
9797
Expression operand = unary.getExpression();
98-
Expression simplifiedOperand = simplify(operand, nonZeroTerms);
98+
Expression simplifiedOperand = simplify(operand, nonZeroExpressions);
9999
if (!operand.equals(simplifiedOperand))
100100
return new UnaryExpression(unary.getOp(), simplifiedOperand);
101101

@@ -109,19 +109,19 @@ private static Expression simplifyUnary(UnaryExpression unary, List<Expression>
109109
/**
110110
* Simplifies a ternary expression by visiting condition, then branch, and else branch.
111111
*/
112-
private static Expression simplifyIte(Ite ite, List<Expression> nonZeroTerms) {
112+
private static Expression simplifyIte(Ite ite, List<Expression> nonZeroExpressions) {
113113
Expression condition = ite.getCondition();
114-
Expression simplifiedCondition = simplify(condition, nonZeroTerms);
114+
Expression simplifiedCondition = simplify(condition, nonZeroExpressions);
115115
if (!condition.equals(simplifiedCondition))
116116
return new Ite(simplifiedCondition, ite.getThen().clone(), ite.getElse().clone());
117117

118118
Expression thenExpression = ite.getThen();
119-
Expression simplifiedThen = simplify(thenExpression, nonZeroTerms);
119+
Expression simplifiedThen = simplify(thenExpression, nonZeroExpressions);
120120
if (!thenExpression.equals(simplifiedThen))
121121
return new Ite(condition.clone(), simplifiedThen, ite.getElse().clone());
122122

123123
Expression elseExpression = ite.getElse();
124-
Expression simplifiedElse = simplify(elseExpression, nonZeroTerms);
124+
Expression simplifiedElse = simplify(elseExpression, nonZeroExpressions);
125125
if (!elseExpression.equals(simplifiedElse))
126126
return new Ite(condition.clone(), thenExpression.clone(), simplifiedElse);
127127

@@ -131,9 +131,9 @@ private static Expression simplifyIte(Ite ite, List<Expression> nonZeroTerms) {
131131
/**
132132
* Simplifies an expression wrapped in parentheses while preserving the group node.
133133
*/
134-
private static Expression simplifyGroup(GroupExpression group, List<Expression> nonZeroTerms) {
134+
private static Expression simplifyGroup(GroupExpression group, List<Expression> nonZeroExpressions) {
135135
Expression expression = group.getExpression();
136-
Expression simplified = simplify(expression, nonZeroTerms);
136+
Expression simplified = simplify(expression, nonZeroExpressions);
137137
if (!expression.equals(simplified))
138138
return new GroupExpression(simplified);
139139
return group.clone();
@@ -143,13 +143,13 @@ private static Expression simplifyGroup(GroupExpression group, List<Expression>
143143
* Dispatches a local binary arithmetic identity by operator.
144144
*/
145145
private static Expression simplifyLocalBinary(Expression left, Expression right, String op,
146-
List<Expression> nonZeroTerms) {
146+
List<Expression> nonZeroExpressions) {
147147
return switch (op) {
148148
case "+" -> simplifyAddition(left, right);
149149
case "-" -> simplifySubtraction(left, right);
150150
case "*" -> simplifyMultiplication(left, right);
151-
case "/" -> simplifyDivision(left, right, nonZeroTerms);
152-
case "%" -> simplifyModulo(left, right, nonZeroTerms);
151+
case "/" -> simplifyDivision(left, right, nonZeroExpressions);
152+
case "%" -> simplifyModulo(left, right, nonZeroExpressions);
153153
default -> null;
154154
};
155155
}
@@ -217,52 +217,52 @@ private static Expression simplifyMultiplication(Expression left, Expression rig
217217
/**
218218
* Applies division identities, using prior non-zero premises when needed.
219219
*/
220-
private static Expression simplifyDivision(Expression left, Expression right, List<Expression> nonZeroTerms) {
220+
private static Expression simplifyDivision(Expression left, Expression right, List<Expression> nonZeroExpressions) {
221221
// x / 1 -> x
222222
if (isOne(right))
223223
return left.clone();
224224
// 0 / x -> 0 (x != 0)
225-
if (isZero(left) && isKnownNonZero(right, nonZeroTerms))
225+
if (isZero(left) && isNonZero(right, nonZeroExpressions))
226226
return left.clone();
227227
// x / x -> 1 (x != 0)
228-
if (left.equals(right) && isKnownNonZero(right, nonZeroTerms))
228+
if (left.equals(right) && isNonZero(right, nonZeroExpressions))
229229
return new LiteralInt(1);
230230
return null;
231231
}
232232

233233
/**
234234
* Applies modulo identities, using prior non-zero premises when needed.
235235
*/
236-
private static Expression simplifyModulo(Expression left, Expression right, List<Expression> nonZeroTerms) {
236+
private static Expression simplifyModulo(Expression left, Expression right, List<Expression> nonZeroExpressions) {
237237
// x % 1 -> 0
238238
if (isOne(right))
239239
return new LiteralInt(0);
240240
// x % x -> 0 (x != 0)
241-
if (left.equals(right) && isKnownNonZero(right, nonZeroTerms))
241+
if (left.equals(right) && isNonZero(right, nonZeroExpressions))
242242
return new LiteralInt(0);
243243
return null;
244244
}
245245

246246
/**
247247
* Records direct non-zero premises shaped as expr != 0 or 0 != expr.
248248
*/
249-
private static void addNonZeroTerm(Expression expression, List<Expression> nonZeroTerms) {
249+
private static void addNonZeroExpression(Expression expression, List<Expression> nonZeroExpressions) {
250250
if (!(expression instanceof BinaryExpression binary) || !"!=".equals(binary.getOperator()))
251251
return;
252252

253253
Expression left = binary.getFirstOperand();
254254
Expression right = binary.getSecondOperand();
255255
if (isZero(left))
256-
nonZeroTerms.add(right.clone());
256+
nonZeroExpressions.add(right.clone());
257257
if (isZero(right))
258-
nonZeroTerms.add(left.clone());
258+
nonZeroExpressions.add(left.clone());
259259
}
260260

261261
/**
262262
* Checks whether a previous premise recorded an expression as non-zero.
263263
*/
264-
private static boolean isKnownNonZero(Expression expression, List<Expression> nonZeroTerms) {
265-
return nonZeroTerms.stream().anyMatch(term -> term.equals(expression));
264+
private static boolean isNonZero(Expression expression, List<Expression> nonZeroExpressions) {
265+
return nonZeroExpressions.stream().anyMatch(e -> e.equals(expression));
266266
}
267267

268268
/**

0 commit comments

Comments
 (0)