Method iteExample

examples/java/JavaGenericExample.java:1306–1317

(Context ctx)

    // / Create an ite-Expr (if-then-else Exprs).

    public void iteExample(Context ctx)
    {
        System.out.println("ITEExample");
        Log.append("ITEExample");

        BoolExpr f = ctx.mkFalse();
        IntNum one = ctx.mkInt(1);
        IntNum zero = ctx.mkInt(0);
        Expr<IntSort> ite = ctx.mkITE(f, one, zero);

        System.out.printf("Expr: %s%n", ite);
    }

    // / Create an enumeration data type.