Skip to content

Commit cb0cb2e

Browse files
committed
Update VCImplicationGenerator
1 parent ee3919c commit cb0cb2e

1 file changed

Lines changed: 6 additions & 6 deletions

File tree

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,11 @@
99

1010
public class VCImplicationGenerator extends Generator<VCImplication> {
1111

12-
static final String[] BINDERS = { "x", "y", "z" };
13-
static final String[] FREE_VARS = { "a", "b", "c" };
12+
public static final String[] BINDERS = { "x", "y", "z", "w" };
13+
public static final String[] FREE_VARS = { "a", "b", "c", "d" };
1414
private static final String[] COMPARISON_OPS = { "==", "!=", ">=", ">", "<=", "<" };
15+
private static final String[] BOOLEAN_OPS = { "&&", "||", "-->", "==", "!=" };
16+
private static final String[] ARITHMETIC_OPS = { "+", "-", "*" };
1517

1618
public VCImplicationGenerator() {
1719
super(VCImplication.class);
@@ -69,8 +71,7 @@ private static String foldableComparison(SourceOfRandomness random) {
6971
private static String foldableBoolean(SourceOfRandomness random) {
7072
String left = random.nextBoolean() ? "true" : "false";
7173
String right = random.nextBoolean() ? "true" : "false";
72-
String[] ops = { "&&", "||", "-->", "==", "!=" };
73-
return left + " " + ops[random.nextInt(0, ops.length - 1)] + " " + right;
74+
return left + " " + BOOLEAN_OPS[random.nextInt(0, BOOLEAN_OPS.length - 1)] + " " + right;
7475
}
7576

7677
private static String foldableIte(SourceOfRandomness random) {
@@ -83,8 +84,7 @@ private static String foldableIte(SourceOfRandomness random) {
8384
private static String literalArithmetic(SourceOfRandomness random) {
8485
String left = intLiteral(random);
8586
String right = Integer.toString(random.nextInt(1, 7));
86-
String[] ops = { "+", "-", "*" };
87-
return left + " " + ops[random.nextInt(0, ops.length - 1)] + " " + right;
87+
return left + " " + ARITHMETIC_OPS[random.nextInt(0, ARITHMETIC_OPS.length - 1)] + " " + right;
8888
}
8989

9090
private static String adjacentConstants(SourceOfRandomness random) {

0 commit comments

Comments
 (0)