Skip to content

Commit b813bb7

Browse files
rcosta358rcosta358
committed
Add VC Arithmetic Simplification
1 parent 9fc831a commit b813bb7

5 files changed

Lines changed: 445 additions & 3 deletions

File tree

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

Lines changed: 284 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,284 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import java.util.ArrayList;
4+
import java.util.List;
5+
6+
import liquidjava.processor.SimplifiedVCImplication;
7+
import liquidjava.processor.VCImplication;
8+
import liquidjava.rj_language.Predicate;
9+
import liquidjava.rj_language.ast.BinaryExpression;
10+
import liquidjava.rj_language.ast.Expression;
11+
import liquidjava.rj_language.ast.GroupExpression;
12+
import liquidjava.rj_language.ast.Ite;
13+
import liquidjava.rj_language.ast.LiteralInt;
14+
import liquidjava.rj_language.ast.LiteralReal;
15+
import liquidjava.rj_language.ast.UnaryExpression;
16+
17+
/**
18+
* Simplifies VCImplication chains by applying arithmetic identities inside refinements.
19+
*/
20+
public class VCArithmeticSimplification {
21+
22+
/**
23+
* Applies the first arithmetic simplification available in a VC chain.
24+
*/
25+
public static VCImplication apply(VCImplication implication) {
26+
if (implication == null)
27+
return null;
28+
29+
return apply(implication, List.of());
30+
}
31+
32+
private static VCImplication apply(VCImplication implication, List<Expression> nonZeroTerms) {
33+
if (implication == null)
34+
return null;
35+
36+
Expression expression = implication.getRefinement().getExpression();
37+
Expression simplified = simplify(expression, nonZeroTerms);
38+
if (!expression.equals(simplified)) {
39+
VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified),
40+
implication.getOrigin());
41+
result.setNext(implication.getNext() == null ? null : implication.getNext().clone());
42+
return result;
43+
}
44+
45+
List<Expression> nextNonZeroTerms = new ArrayList<>(nonZeroTerms);
46+
addNonZeroTerm(implication.getRefinement().getExpression(), nextNonZeroTerms);
47+
48+
VCImplication next = apply(implication.getNext(), nextNonZeroTerms);
49+
if (implication.getNext() == null || implication.getNext().equals(next))
50+
return implication;
51+
52+
VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone());
53+
result.setNext(next);
54+
return result;
55+
}
56+
57+
/**
58+
* Simplifies the first arithmetic identity found inside an expression.
59+
*/
60+
private static Expression simplify(Expression expression, List<Expression> nonZeroTerms) {
61+
if (expression instanceof BinaryExpression binary)
62+
return simplifyBinary(binary, nonZeroTerms);
63+
if (expression instanceof UnaryExpression unary)
64+
return simplifyUnary(unary, nonZeroTerms);
65+
if (expression instanceof Ite ite)
66+
return simplifyIte(ite, nonZeroTerms);
67+
if (expression instanceof GroupExpression group)
68+
return simplifyGroup(group, nonZeroTerms);
69+
return expression.clone();
70+
}
71+
72+
/**
73+
* Simplifies a binary expression by visiting operands before the current node.
74+
*/
75+
private static Expression simplifyBinary(BinaryExpression binary, List<Expression> nonZeroTerms) {
76+
Expression left = binary.getFirstOperand();
77+
Expression simplifiedLeft = simplify(left, nonZeroTerms);
78+
if (!left.equals(simplifiedLeft))
79+
return new BinaryExpression(simplifiedLeft, binary.getOperator(), binary.getSecondOperand().clone());
80+
81+
Expression right = binary.getSecondOperand();
82+
Expression simplifiedRight = simplify(right, nonZeroTerms);
83+
if (!right.equals(simplifiedRight))
84+
return new BinaryExpression(left.clone(), binary.getOperator(), simplifiedRight);
85+
86+
Expression simplifiedBinary = simplifyLocalBinary(left, right, binary.getOperator(), nonZeroTerms);
87+
if (simplifiedBinary != null)
88+
return simplifiedBinary;
89+
90+
return new BinaryExpression(left.clone(), binary.getOperator(), right.clone());
91+
}
92+
93+
/**
94+
* Simplifies a unary expression by visiting its operand before the current node.
95+
*/
96+
private static Expression simplifyUnary(UnaryExpression unary, List<Expression> nonZeroTerms) {
97+
Expression operand = unary.getExpression();
98+
Expression simplifiedOperand = simplify(operand, nonZeroTerms);
99+
if (!operand.equals(simplifiedOperand))
100+
return new UnaryExpression(unary.getOp(), simplifiedOperand);
101+
102+
if ("-".equals(unary.getOp()) && isNegation(operand))
103+
return negatedExpression(operand).clone();
104+
105+
return new UnaryExpression(unary.getOp(), operand.clone());
106+
}
107+
108+
/**
109+
* Simplifies a ternary expression by visiting condition, then branch, and else branch.
110+
*/
111+
private static Expression simplifyIte(Ite ite, List<Expression> nonZeroTerms) {
112+
Expression condition = ite.getCondition();
113+
Expression simplifiedCondition = simplify(condition, nonZeroTerms);
114+
if (!condition.equals(simplifiedCondition))
115+
return new Ite(simplifiedCondition, ite.getThen().clone(), ite.getElse().clone());
116+
117+
Expression thenExpression = ite.getThen();
118+
Expression simplifiedThen = simplify(thenExpression, nonZeroTerms);
119+
if (!thenExpression.equals(simplifiedThen))
120+
return new Ite(condition.clone(), simplifiedThen, ite.getElse().clone());
121+
122+
Expression elseExpression = ite.getElse();
123+
Expression simplifiedElse = simplify(elseExpression, nonZeroTerms);
124+
if (!elseExpression.equals(simplifiedElse))
125+
return new Ite(condition.clone(), thenExpression.clone(), simplifiedElse);
126+
127+
return new Ite(condition.clone(), thenExpression.clone(), elseExpression.clone());
128+
}
129+
130+
/**
131+
* Simplifies an expression wrapped in parentheses while preserving the group node.
132+
*/
133+
private static Expression simplifyGroup(GroupExpression group, List<Expression> nonZeroTerms) {
134+
Expression expression = group.getExpression();
135+
Expression simplified = simplify(expression, nonZeroTerms);
136+
if (!expression.equals(simplified))
137+
return new GroupExpression(simplified);
138+
return group.clone();
139+
}
140+
141+
/**
142+
* Dispatches a local binary arithmetic identity by operator.
143+
*/
144+
private static Expression simplifyLocalBinary(Expression left, Expression right, String op,
145+
List<Expression> nonZeroTerms) {
146+
return switch (op) {
147+
case "+" -> simplifyAddition(left, right);
148+
case "-" -> simplifySubtraction(left, right);
149+
case "*" -> simplifyMultiplication(left, right);
150+
case "/" -> simplifyDivision(left, right, nonZeroTerms);
151+
case "%" -> simplifyModulo(left, right, nonZeroTerms);
152+
default -> null;
153+
};
154+
}
155+
156+
/**
157+
* Applies addition identities involving zero and unary negation.
158+
*/
159+
private static Expression simplifyAddition(Expression left, Expression right) {
160+
if (isZero(right))
161+
return left.clone();
162+
if (isZero(left))
163+
return right.clone();
164+
if (isNegation(right) && left.equals(negatedExpression(right)))
165+
return new LiteralInt(0);
166+
if (isNegation(left) && negatedExpression(left).equals(right))
167+
return new LiteralInt(0);
168+
if (isNegation(right))
169+
return new BinaryExpression(left.clone(), "-", negatedExpression(right).clone());
170+
return null;
171+
}
172+
173+
/**
174+
* Applies subtraction identities involving zero, same operands, and unary negation.
175+
*/
176+
private static Expression simplifySubtraction(Expression left, Expression right) {
177+
if (isZero(right))
178+
return left.clone();
179+
if (isZero(left))
180+
return new UnaryExpression("-", right.clone());
181+
if (left.equals(right))
182+
return new LiteralInt(0);
183+
if (isNegation(right))
184+
return new BinaryExpression(left.clone(), "+", negatedExpression(right).clone());
185+
return null;
186+
}
187+
188+
/**
189+
* Applies multiplication identities involving one and zero.
190+
*/
191+
private static Expression simplifyMultiplication(Expression left, Expression right) {
192+
if (isOne(right))
193+
return left.clone();
194+
if (isOne(left))
195+
return right.clone();
196+
if (isZero(right))
197+
return right.clone();
198+
if (isZero(left))
199+
return left.clone();
200+
return null;
201+
}
202+
203+
/**
204+
* Applies division identities, using prior non-zero premises when needed.
205+
*/
206+
private static Expression simplifyDivision(Expression left, Expression right, List<Expression> nonZeroTerms) {
207+
if (isOne(right))
208+
return left.clone();
209+
if (isZero(left) && isKnownNonZero(right, nonZeroTerms))
210+
return left.clone();
211+
if (left.equals(right) && isKnownNonZero(right, nonZeroTerms))
212+
return new LiteralInt(1);
213+
return null;
214+
}
215+
216+
/**
217+
* Applies modulo identities, using prior non-zero premises when needed.
218+
*/
219+
private static Expression simplifyModulo(Expression left, Expression right, List<Expression> nonZeroTerms) {
220+
if (isOne(right))
221+
return new LiteralInt(0);
222+
if (left.equals(right) && isKnownNonZero(right, nonZeroTerms))
223+
return new LiteralInt(0);
224+
return null;
225+
}
226+
227+
/**
228+
* Records direct non-zero premises shaped as expr != 0 or 0 != expr.
229+
*/
230+
private static void addNonZeroTerm(Expression expression, List<Expression> nonZeroTerms) {
231+
if (!(expression instanceof BinaryExpression binary) || !"!=".equals(binary.getOperator()))
232+
return;
233+
234+
Expression left = binary.getFirstOperand();
235+
Expression right = binary.getSecondOperand();
236+
if (isZero(left))
237+
nonZeroTerms.add(right.clone());
238+
if (isZero(right))
239+
nonZeroTerms.add(left.clone());
240+
}
241+
242+
/**
243+
* Checks whether a previous premise recorded an expression as non-zero.
244+
*/
245+
private static boolean isKnownNonZero(Expression expression, List<Expression> nonZeroTerms) {
246+
return nonZeroTerms.stream().anyMatch(term -> term.equals(expression));
247+
}
248+
249+
/**
250+
* Checks whether an expression is a numeric zero literal.
251+
*/
252+
private static boolean isZero(Expression expression) {
253+
if (expression instanceof LiteralInt literal)
254+
return literal.getValue() == 0;
255+
if (expression instanceof LiteralReal literal)
256+
return literal.getValue() == 0.0;
257+
return false;
258+
}
259+
260+
/**
261+
* Checks whether an expression is a numeric one literal.
262+
*/
263+
private static boolean isOne(Expression expression) {
264+
if (expression instanceof LiteralInt literal)
265+
return literal.getValue() == 1;
266+
if (expression instanceof LiteralReal literal)
267+
return literal.getValue() == 1.0;
268+
return false;
269+
}
270+
271+
/**
272+
* Checks whether an expression is unary negation.
273+
*/
274+
private static boolean isNegation(Expression expression) {
275+
return expression instanceof UnaryExpression unary && "-".equals(unary.getOp());
276+
}
277+
278+
/**
279+
* Reads the operand of a unary negation expression.
280+
*/
281+
private static Expression negatedExpression(Expression expression) {
282+
return ((UnaryExpression) expression).getExpression();
283+
}
284+
}

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

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -31,11 +31,17 @@ public static VCImplication simplifyOnce(VCImplication implication) {
3131
if (implication == null)
3232
return null;
3333

34-
// first try to apply substitution, then folding
34+
// substitution
3535
VCImplication substituted = VCSubstitution.apply(implication);
3636
if (!implication.equals(substituted))
3737
return substituted;
3838

39-
return VCFolding.apply(implication);
39+
// folding
40+
VCImplication folded = VCFolding.apply(implication);
41+
if (!implication.equals(folded))
42+
return folded;
43+
44+
// arithmetic simplification
45+
return VCArithmeticSimplification.apply(implication);
4046
}
4147
}

0 commit comments

Comments
 (0)