VCImplicationGenerator.java

package liquidjava.rj_language.opt;

import static liquidjava.utils.VCTestUtils.vc;

import com.pholser.junit.quickcheck.generator.GenerationStatus;
import com.pholser.junit.quickcheck.generator.Generator;
import com.pholser.junit.quickcheck.random.SourceOfRandomness;
import liquidjava.processor.VCImplication;

public class VCImplicationGenerator extends Generator<VCImplication> {

    public static final String[] BINDERS = { "x", "y", "z", "w" };
    public static final String[] FREE_VARS = { "a", "b", "c", "d" };
    public static final String[] FUNCTIONS = { "f", "g" };
    private static final String[] COMPARISON_OPS = { "==", "!=", ">=", ">", "<=", "<" };
    private static final String[] BOOLEAN_OPS = { "&&", "||", "-->", "==", "!=" };
    private static final String[] ARITHMETIC_OPS = { "+", "-", "*" };

    public VCImplicationGenerator() {
        super(VCImplication.class);
    }

    @Override
    public VCImplication generate(SourceOfRandomness random, GenerationStatus status) {
        return switch (random.nextInt(0, 18)) {
        case 0 -> vc(substitution(random, "x"), comparison(random, "x"));
        case 1 -> vc(reverseSubstitution(random, "x"), comparison(random, "x"));
        case 2 -> vc(nonSubstitution(random, "x"), substitution(random, "y"), comparison(random, "y"));
        case 3 -> vc(substitution(random, "x"), dependentSubstitution(random), comparison(random, "y"));
        case 4 -> vc("∀y:int. true", "∀x:int. x == y + 1", comparison(random, "x"));
        case 5 -> vc(foldableComparison(random));
        case 6 -> vc(foldableBoolean(random), comparison(random, "x"));
        case 7 -> vc(foldableIte(random));
        case 8 -> vc(adjacentConstants(random) + " " + comparisonOperator(random) + " " + intLiteral(random));
        case 9 -> vc(arithmeticIdentity(random));
        case 10 -> guardedArithmeticIdentity(random);
        case 11 -> vc(logicalIdentity(random));
        case 12 -> vc(unusedTrueBinder(random));
        case 13 -> vc(falseBinder(random));
        case 14 -> exactFunctionSubstitution(random);
        case 15 -> reverseFunctionSubstitution(random);
        case 16 -> chainedFunctionSubstitution(random);
        case 17 -> differentArgumentFunctionSubstitution(random);
        case 18 -> recursiveFunctionSubstitution(random);
        default -> vc(substitution(random, "x"), substitution(random, "y"), foldableComparison(random));
        };
    }

    private static String substitution(SourceOfRandomness random, String binder) {
        String value = value(random);
        if (random.nextBoolean())
            return "∀" + binder + ":int. " + binder + " == " + value;
        return "∀" + binder + ":int. " + value + " == " + binder;
    }

    private static String reverseSubstitution(SourceOfRandomness random, String binder) {
        return "∀" + binder + ":int. " + value(random) + " == " + binder;
    }

    private static String dependentSubstitution(SourceOfRandomness random) {
        int offset = random.nextInt(-3, 3);
        return "∀y:int. y == x " + signed(offset);
    }

    private static String nonSubstitution(SourceOfRandomness random, String binder) {
        if (random.nextBoolean())
            return "∀" + binder + ":int. " + binder + " > " + intLiteral(random);
        return "∀" + binder + ":int. " + binder + " == " + binder + " " + signed(random.nextInt(1, 5));
    }

    private static VCImplication exactFunctionSubstitution(SourceOfRandomness random) {
        String function = functionName(random);
        return vc(functionSubstitution(random, function, "a"), functionUse(random, function, "a"));
    }

    private static VCImplication reverseFunctionSubstitution(SourceOfRandomness random) {
        String function = functionName(random);
        return vc(reverseFunctionSubstitution(random, function, "a"), functionUse(random, function, "a"));
    }

    private static VCImplication chainedFunctionSubstitution(SourceOfRandomness random) {
        String function = functionName(random);
        return vc(functionSubstitution(random, function, "a"), dependentFunctionSubstitution(random, function),
                functionUse(random, function, "b"));
    }

    private static VCImplication differentArgumentFunctionSubstitution(SourceOfRandomness random) {
        String function = functionName(random);
        return vc(functionSubstitution(random, function, "a"), functionUse(random, function, "b"));
    }

    private static VCImplication recursiveFunctionSubstitution(SourceOfRandomness random) {
        String function = functionName(random);
        String invocation = functionInvocation(function, "a");
        return vc(invocation + " == " + invocation + " " + signed(random.nextInt(1, 5)),
                functionUse(random, function, "a"));
    }

    private static String functionSubstitution(SourceOfRandomness random, String function, String argument) {
        return functionInvocation(function, argument) + " == " + value(random);
    }

    private static String reverseFunctionSubstitution(SourceOfRandomness random, String function, String argument) {
        return value(random) + " == " + functionInvocation(function, argument);
    }

    private static String dependentFunctionSubstitution(SourceOfRandomness random, String function) {
        return functionInvocation(function, "b") + " == " + functionInvocation(function, "a") + " "
                + signed(random.nextInt(-3, 3));
    }

    private static String functionUse(SourceOfRandomness random, String function, String argument) {
        return functionInvocation(function, argument) + " " + comparisonOperator(random) + " " + intLiteral(random);
    }

    private static String functionInvocation(String function, String argument) {
        return function + "(" + argument + ")";
    }

    private static String functionName(SourceOfRandomness random) {
        return FUNCTIONS[random.nextInt(0, FUNCTIONS.length - 1)];
    }

    private static String[] unusedTrueBinder(SourceOfRandomness random) {
        return new String[] { "∀x:int. true", comparison(random, "a") };
    }

    private static String[] falseBinder(SourceOfRandomness random) {
        return new String[] { "∀x:int. false", comparison(random, "x") };
    }

    private static String comparison(SourceOfRandomness random, String preferredVar) {
        String left = random.nextBoolean() ? preferredVar : arithmetic(random, preferredVar);
        String right = random.nextBoolean() ? intLiteral(random)
                : arithmetic(random, FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)]);
        return left + " " + comparisonOperator(random) + " " + right;
    }

    private static String foldableComparison(SourceOfRandomness random) {
        return literalArithmetic(random) + " " + comparisonOperator(random) + " " + literalArithmetic(random);
    }

    private static String foldableBoolean(SourceOfRandomness random) {
        String left = random.nextBoolean() ? "true" : "false";
        String right = random.nextBoolean() ? "true" : "false";
        return left + " " + BOOLEAN_OPS[random.nextInt(0, BOOLEAN_OPS.length - 1)] + " " + right;
    }

    private static String foldableIte(SourceOfRandomness random) {
        String condition = random.nextBoolean() ? foldableBoolean(random) : foldableComparison(random);
        String thenBranch = comparison(random, "x");
        String elseBranch = random.nextBoolean() ? thenBranch : comparison(random, "y");
        return condition + " ? " + thenBranch + " : " + elseBranch;
    }

    private static String literalArithmetic(SourceOfRandomness random) {
        String left = intLiteral(random);
        String right = Integer.toString(random.nextInt(1, 7));
        return left + " " + ARITHMETIC_OPS[random.nextInt(0, ARITHMETIC_OPS.length - 1)] + " " + right;
    }

    private static String adjacentConstants(SourceOfRandomness random) {
        String variable = FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)];
        int left = random.nextInt(-3, 3);
        int right = random.nextInt(-3, 3);
        return variable + " " + signed(left) + " " + signed(right);
    }

    private static String arithmeticIdentity(SourceOfRandomness random) {
        String var = FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)];
        String other = FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)];
        return switch (random.nextInt(0, 9)) {
        case 0 -> var + " + 0 " + comparisonOperator(random) + " " + intLiteral(random);
        case 1 -> "0 + " + var + " " + comparisonOperator(random) + " " + intLiteral(random);
        case 2 -> var + " - 0 " + comparisonOperator(random) + " " + intLiteral(random);
        case 3 -> "0 - " + var + " " + comparisonOperator(random) + " " + intLiteral(random);
        case 4 -> var + " - " + var + " == 0";
        case 5 -> var + " * 1 " + comparisonOperator(random) + " " + intLiteral(random);
        case 6 -> "1 * " + var + " " + comparisonOperator(random) + " " + intLiteral(random);
        case 7 -> var + " * 0 == 0";
        case 8 -> var + " / 1 " + comparisonOperator(random) + " " + intLiteral(random);
        default -> var + " + -" + other + " " + comparisonOperator(random) + " " + intLiteral(random);
        };
    }

    private static VCImplication guardedArithmeticIdentity(SourceOfRandomness random) {
        String var = FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)];
        String guard = random.nextBoolean() ? var + " != 0" : "0 != " + var;
        String use = switch (random.nextInt(0, 2)) {
        case 0 -> "0 / " + var + " == 0";
        case 1 -> var + " / " + var + " == 1";
        default -> var + " % " + var + " == 0";
        };
        return vc(guard, use);
    }

    private static String logicalIdentity(SourceOfRandomness random) {
        String predicate = "(" + comparison(random, FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)]) + ")";
        return switch (random.nextInt(0, 16)) {
        case 0 -> predicate + " && true";
        case 1 -> "true && " + predicate;
        case 2 -> predicate + " && false";
        case 3 -> "false && " + predicate;
        case 4 -> predicate + " || true";
        case 5 -> "true || " + predicate;
        case 6 -> predicate + " || false";
        case 7 -> "false || " + predicate;
        case 8 -> predicate + " && " + predicate;
        case 9 -> predicate + " || " + predicate;
        case 10 -> predicate + " --> true";
        case 11 -> "false --> " + predicate;
        case 12 -> "true --> " + predicate;
        case 13 -> predicate + " --> " + predicate;
        case 14 -> predicate + " == " + predicate;
        case 15 -> predicate + " != " + predicate;
        default -> "!!" + predicate;
        };
    }

    private static String comparisonOperator(SourceOfRandomness random) {
        return COMPARISON_OPS[random.nextInt(0, COMPARISON_OPS.length - 1)];
    }

    private static String value(SourceOfRandomness random) {
        String var = FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)];
        return switch (random.nextInt(0, 3)) {
        case 0 -> intLiteral(random);
        case 1 -> var;
        case 2 -> var + " " + signed(random.nextInt(-4, 4));
        default -> arithmetic(random, var);
        };
    }

    private static String arithmetic(SourceOfRandomness random, String var) {
        int constant = random.nextInt(-3, 3);
        return switch (random.nextInt(0, 2)) {
        case 0 -> var + " " + signed(constant);
        case 1 -> var + " * " + random.nextInt(1, 5);
        default -> "(" + var + " " + signed(constant) + ")";
        };
    }

    private static String signed(int value) {
        if (value < 0)
            return "- " + Math.abs(value);
        return "+ " + value;
    }

    private static String intLiteral(SourceOfRandomness random) {
        return Integer.toString(random.nextInt(-7, 7));
    }
}