Skip to content

Commit eb9ff24

Browse files
rcosta358rcosta358
committed
Add VC Logical Simplification
1 parent 334ff7e commit eb9ff24

5 files changed

Lines changed: 400 additions & 2 deletions

File tree

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

Lines changed: 252 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,252 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import liquidjava.processor.SimplifiedVCImplication;
4+
import liquidjava.processor.VCImplication;
5+
import liquidjava.rj_language.Predicate;
6+
import liquidjava.rj_language.ast.BinaryExpression;
7+
import liquidjava.rj_language.ast.Expression;
8+
import liquidjava.rj_language.ast.GroupExpression;
9+
import liquidjava.rj_language.ast.Ite;
10+
import liquidjava.rj_language.ast.LiteralBoolean;
11+
import liquidjava.rj_language.ast.UnaryExpression;
12+
13+
/**
14+
* Simplifies VCImplication chains by applying logical identities inside refinements
15+
*/
16+
public class VCLogicalSimplification {
17+
18+
/**
19+
* Applies the first logical simplification available in a VC chain
20+
*/
21+
public static VCImplication apply(VCImplication implication) {
22+
if (implication == null)
23+
return null;
24+
25+
Expression expression = implication.getRefinement().getExpression();
26+
Expression simplified = simplify(expression);
27+
if (!expression.equals(simplified)) {
28+
VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified),
29+
implication.getOrigin());
30+
result.setNext(implication.getNext() == null ? null : implication.getNext().clone());
31+
return result;
32+
}
33+
34+
VCImplication next = apply(implication.getNext());
35+
if (implication.getNext() == null || implication.getNext().equals(next))
36+
return implication;
37+
38+
VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone());
39+
result.setNext(next);
40+
return result;
41+
}
42+
43+
/**
44+
* Simplifies the first logical identity found inside an expression
45+
*/
46+
private static Expression simplify(Expression expression) {
47+
if (expression instanceof BinaryExpression binary)
48+
return simplifyBinary(binary);
49+
if (expression instanceof UnaryExpression unary)
50+
return simplifyUnary(unary);
51+
if (expression instanceof Ite ite)
52+
return simplifyIte(ite);
53+
if (expression instanceof GroupExpression group)
54+
return simplifyGroup(group);
55+
return expression.clone();
56+
}
57+
58+
/**
59+
* Simplifies a binary expression by visiting operands before the current node
60+
*/
61+
private static Expression simplifyBinary(BinaryExpression binary) {
62+
Expression left = binary.getFirstOperand();
63+
Expression simplifiedLeft = simplify(left);
64+
if (!left.equals(simplifiedLeft))
65+
return new BinaryExpression(simplifiedLeft, binary.getOperator(), binary.getSecondOperand().clone());
66+
67+
Expression right = binary.getSecondOperand();
68+
Expression simplifiedRight = simplify(right);
69+
if (!right.equals(simplifiedRight))
70+
return new BinaryExpression(left.clone(), binary.getOperator(), simplifiedRight);
71+
72+
Expression simplifiedBinary = simplifyLocalBinary(left, right, binary.getOperator());
73+
if (simplifiedBinary != null)
74+
return simplifiedBinary;
75+
76+
return new BinaryExpression(left.clone(), binary.getOperator(), right.clone());
77+
}
78+
79+
/**
80+
* Simplifies a unary expression by visiting its operand before the current node
81+
*/
82+
private static Expression simplifyUnary(UnaryExpression unary) {
83+
Expression operand = unary.getExpression();
84+
Expression simplifiedOperand = simplify(operand);
85+
if (!operand.equals(simplifiedOperand))
86+
return new UnaryExpression(unary.getOp(), simplifiedOperand);
87+
88+
// !!x -> x
89+
if ("!".equals(unary.getOp()) && isNot(operand))
90+
return negatedExpression(operand).clone();
91+
92+
return new UnaryExpression(unary.getOp(), operand.clone());
93+
}
94+
95+
/**
96+
* Simplifies a ternary expression by visiting condition, then branch, and else branch
97+
*/
98+
private static Expression simplifyIte(Ite ite) {
99+
Expression condition = ite.getCondition();
100+
Expression simplifiedCondition = simplify(condition);
101+
if (!condition.equals(simplifiedCondition))
102+
return new Ite(simplifiedCondition, ite.getThen().clone(), ite.getElse().clone());
103+
104+
Expression thenExpression = ite.getThen();
105+
Expression simplifiedThen = simplify(thenExpression);
106+
if (!thenExpression.equals(simplifiedThen))
107+
return new Ite(condition.clone(), simplifiedThen, ite.getElse().clone());
108+
109+
Expression elseExpression = ite.getElse();
110+
Expression simplifiedElse = simplify(elseExpression);
111+
if (!elseExpression.equals(simplifiedElse))
112+
return new Ite(condition.clone(), thenExpression.clone(), simplifiedElse);
113+
114+
return new Ite(condition.clone(), thenExpression.clone(), elseExpression.clone());
115+
}
116+
117+
/**
118+
* Simplifies an expression wrapped in parentheses while preserving the group node
119+
*/
120+
private static Expression simplifyGroup(GroupExpression group) {
121+
Expression expression = group.getExpression();
122+
Expression simplified = simplify(expression);
123+
if (!expression.equals(simplified))
124+
return new GroupExpression(simplified);
125+
return group.clone();
126+
}
127+
128+
/**
129+
* Dispatches a local binary logical identity by operator
130+
*/
131+
private static Expression simplifyLocalBinary(Expression left, Expression right, String op) {
132+
return switch (op) {
133+
case "&&" -> simplifyConjunction(left, right);
134+
case "||" -> simplifyDisjunction(left, right);
135+
case "==" -> simplifyEquality(left, right);
136+
case "!=" -> simplifyInequality(left, right);
137+
case "-->" -> simplifyImplication(left, right);
138+
default -> null;
139+
};
140+
}
141+
142+
/**
143+
* Applies conjunction identities involving boolean literals and same operands
144+
*/
145+
private static Expression simplifyConjunction(Expression left, Expression right) {
146+
// x && true -> x
147+
if (isTrue(right))
148+
return left.clone();
149+
// true && x -> x
150+
if (isTrue(left))
151+
return right.clone();
152+
// x && false -> false
153+
if (isFalse(right))
154+
return right.clone();
155+
// false && x -> false
156+
if (isFalse(left))
157+
return left.clone();
158+
// p && p -> p
159+
if (left.equals(right))
160+
return left.clone();
161+
return null;
162+
}
163+
164+
/**
165+
* Applies disjunction identities involving boolean literals and same operands
166+
*/
167+
private static Expression simplifyDisjunction(Expression left, Expression right) {
168+
// x || true -> true
169+
if (isTrue(right))
170+
return right.clone();
171+
// true || x -> true
172+
if (isTrue(left))
173+
return left.clone();
174+
// x || false -> x
175+
if (isFalse(right))
176+
return left.clone();
177+
// false || x -> x
178+
if (isFalse(left))
179+
return right.clone();
180+
// p || p -> p
181+
if (left.equals(right))
182+
return left.clone();
183+
return null;
184+
}
185+
186+
/**
187+
* Applies equality identity for same operands
188+
*/
189+
private static Expression simplifyEquality(Expression left, Expression right) {
190+
// x == x -> true
191+
if (left.equals(right))
192+
return new LiteralBoolean(true);
193+
return null;
194+
}
195+
196+
/**
197+
* Applies inequality identity for same operands
198+
*/
199+
private static Expression simplifyInequality(Expression left, Expression right) {
200+
// x != x -> false
201+
if (left.equals(right))
202+
return new LiteralBoolean(false);
203+
return null;
204+
}
205+
206+
/**
207+
* Applies implication identities involving boolean literals and same operands
208+
*/
209+
private static Expression simplifyImplication(Expression left, Expression right) {
210+
// x --> true -> true
211+
if (isTrue(right))
212+
return right.clone();
213+
// false --> x -> true
214+
if (isFalse(left))
215+
return new LiteralBoolean(true);
216+
// true --> x -> x
217+
if (isTrue(left))
218+
return right.clone();
219+
// x --> x -> true
220+
if (left.equals(right))
221+
return new LiteralBoolean(true);
222+
return null;
223+
}
224+
225+
/**
226+
* Checks whether an expression is true
227+
*/
228+
private static boolean isTrue(Expression expression) {
229+
return expression instanceof LiteralBoolean literal && literal.isBooleanTrue();
230+
}
231+
232+
/**
233+
* Checks whether an expression is false
234+
*/
235+
private static boolean isFalse(Expression expression) {
236+
return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue();
237+
}
238+
239+
/**
240+
* Checks whether an expression is unary logical negation
241+
*/
242+
private static boolean isNot(Expression expression) {
243+
return expression instanceof UnaryExpression unary && "!".equals(unary.getOp());
244+
}
245+
246+
/**
247+
* Returns the operand of a unary logical negation expression
248+
*/
249+
private static Expression negatedExpression(Expression expression) {
250+
return ((UnaryExpression) expression).getExpression();
251+
}
252+
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111
public class VCSimplification {
1212

1313
private static final List<UnaryOperator<VCImplication>> PASSES = List.of(VCSubstitution::apply, VCFolding::apply,
14-
VCArithmeticSimplification::apply);
14+
VCArithmeticSimplification::apply, VCLogicalSimplification::apply);
1515

1616
/**
1717
* Applies all available simplification steps to a VC chain until a fixed point is reached

‎liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java‎

Lines changed: 25 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ public VCImplicationGenerator() {
2121

2222
@Override
2323
public VCImplication generate(SourceOfRandomness random, GenerationStatus status) {
24-
return switch (random.nextInt(0, 11)) {
24+
return switch (random.nextInt(0, 12)) {
2525
case 0 -> vc(substitution(random, "x"), comparison(random, "x"));
2626
case 1 -> vc(reverseSubstitution(random, "x"), comparison(random, "x"));
2727
case 2 -> vc(nonSubstitution(random, "x"), substitution(random, "y"), comparison(random, "y"));
@@ -33,6 +33,7 @@ public VCImplication generate(SourceOfRandomness random, GenerationStatus status
3333
case 8 -> vc(adjacentConstants(random) + " " + comparisonOperator(random) + " " + intLiteral(random));
3434
case 9 -> vc(arithmeticIdentity(random));
3535
case 10 -> guardedArithmeticIdentity(random);
36+
case 11 -> vc(logicalIdentity(random));
3637
default -> vc(substitution(random, "x"), substitution(random, "y"), foldableComparison(random));
3738
};
3839
}
@@ -124,6 +125,29 @@ private static VCImplication guardedArithmeticIdentity(SourceOfRandomness random
124125
return vc(guard, use);
125126
}
126127

128+
private static String logicalIdentity(SourceOfRandomness random) {
129+
String predicate = "(" + comparison(random, FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)]) + ")";
130+
return switch (random.nextInt(0, 16)) {
131+
case 0 -> predicate + " && true";
132+
case 1 -> "true && " + predicate;
133+
case 2 -> predicate + " && false";
134+
case 3 -> "false && " + predicate;
135+
case 4 -> predicate + " || true";
136+
case 5 -> "true || " + predicate;
137+
case 6 -> predicate + " || false";
138+
case 7 -> "false || " + predicate;
139+
case 8 -> predicate + " && " + predicate;
140+
case 9 -> predicate + " || " + predicate;
141+
case 10 -> predicate + " --> true";
142+
case 11 -> "false --> " + predicate;
143+
case 12 -> "true --> " + predicate;
144+
case 13 -> predicate + " --> " + predicate;
145+
case 14 -> predicate + " == " + predicate;
146+
case 15 -> predicate + " != " + predicate;
147+
default -> "!!" + predicate;
148+
};
149+
}
150+
127151
private static String comparisonOperator(SourceOfRandomness random) {
128152
return COMPARISON_OPS[random.nextInt(0, COMPARISON_OPS.length - 1)];
129153
}

0 commit comments

Comments
 (0)