Method parserExample1

examples/java/JavaExample.java:1442–1454

(Context ctx)

    // / Demonstrates how to use the SMTLIB parser.

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

        BoolExpr f = ctx.parseSMTLIB2String(
                "(declare-const x Int) (declare-const y Int) (assert (and (> x y) (> x 0)))",
                null, null, null, null)[0];
        System.out.println("formula " + f);

        @SuppressWarnings("unused")
        Model m = check(ctx, f, Status.SATISFIABLE);
    }

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