Method parserExample2

examples/java/JavaExample.java:1458–1472

(Context ctx)

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

    public void parserExample2(Context ctx) throws TestFailedException
    {
        System.out.println("ParserExample2");
        Log.append("ParserExample2");

        Symbol[] declNames = { ctx.mkSymbol("a"), ctx.mkSymbol("b") };
        FuncDecl a = ctx.mkConstDecl(declNames[0], ctx.mkIntSort());
        FuncDecl b = ctx.mkConstDecl(declNames[1], ctx.mkIntSort());
        FuncDecl[] decls = new FuncDecl[] { a, b };

        BoolExpr f = ctx.parseSMTLIB2String("(assert (> a b))", null, null,
                declNames, decls)[0];
        System.out.println("formula: " + f);
        check(ctx, f, Status.SATISFIABLE);
    }

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