Method parserExample3

examples/java/JavaGenericExample.java:1261–1278

(Context ctx)

    // / Demonstrates how to initialize the parser symbol table.

    public void parserExample3(Context ctx) throws Exception
    {
        System.out.println("ParserExample3");
        Log.append("ParserExample3");

        /* declare function g */
        IntSort I = ctx.mkIntSort();
        FuncDecl<IntSort> g = ctx.mkFuncDecl("g", new Sort[] { I, I }, I);

        BoolExpr ca = commAxiom(ctx, g);

        BoolExpr thm = ctx.parseSMTLIB2String(
                "(declare-fun (Int Int) Int) (assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))",
                null, null, new Symbol[] { ctx.mkSymbol("gg") },
                new FuncDecl[] { g })[0];
        System.out.printf("formula: %s%n", thm);
        prove(ctx, thm, false, ca);
    }


    // / Demonstrates how to handle parser errors using Z3 error handling