Method quantifierExample1

examples/java/JavaGenericExample.java:556–585

(Context ctx)

    // / A basic example of how to use quantifiers.

    @SuppressWarnings("unchecked")
    void quantifierExample1(Context ctx)
    {
        System.out.println("QuantifierExample");
        Log.append("QuantifierExample");

        IntSort[] types = new IntSort[3];
        Arrays.fill(types, ctx.getIntSort());
        Symbol[] names = IntStream.range(0, 3).mapToObj(j -> ctx.mkSymbol(String.format("x_%d", j))).toArray(Symbol[]::new);
        List<Expr<IntSort>> xs = IntStream.range(0, 3).mapToObj(j -> ctx.mkConst(names[j], types[j])).collect(Collectors.toList());
        List<Expr<IntSort>> vars = IntStream.range(0, 3).mapToObj(j -> ctx.mkBound(2 - j, types[j])).collect(Collectors.toList());

        BoolExpr body_vars = ctx.mkAnd(
                ctx.mkEq(ctx.mkAdd(vars.get(0), ctx.mkInt(1)), ctx.mkInt(2)),
                ctx.mkEq(ctx.mkAdd(vars.get(1), ctx.mkInt(2)),
                        ctx.mkAdd(vars.get(2), ctx.mkInt(3))));

        BoolExpr body_const = ctx.mkAnd(
                ctx.mkEq(ctx.mkAdd(xs.get(0), ctx.mkInt(1)), ctx.mkInt(2)),
                ctx.mkEq(ctx.mkAdd(xs.get(1), ctx.mkInt(2)),
                        ctx.mkAdd(xs.get(2), ctx.mkInt(3))));

        Quantifier x = ctx.mkForall(types, names, body_vars, 1, null, null,
                ctx.mkSymbol("Q1"), ctx.mkSymbol("skid1"));
        System.out.printf("Quantifier X: %s%n", x.toString());

        Quantifier y = ctx.mkForall(xs.toArray(new Expr[0]), body_const, 1, null, null,
                ctx.mkSymbol("Q2"), ctx.mkSymbol("skid2"));
        System.out.printf("Quantifier Y: %s%n", y.toString());
    }

    void quantifierExample2(Context ctx)
    {