Method commAxiom

examples/java/JavaExample.java:156–176

(Context ctx, FuncDecl f)

    // construction.
    // / </remarks>
    private BoolExpr commAxiom(Context ctx, FuncDecl f) throws Exception
    {
        Sort t = f.getRange();
        Sort[] dom = f.getDomain();

        if (dom.length != 2 || !t.equals(dom[0]) || !t.equals(dom[1]))
        {
            System.out.println(Integer.toString(dom.length) + " "
                    + dom[0].toString() + " " + dom[1].toString() + " "
                    + t.toString());
            throw new Exception(
                    "function must be binary, and argument types must be equal to return type");
        }

        String bench = "(assert (forall (x " + t.getName()
                + ") (y " + t.getName() + ") (= (" + f.getName() + " x y) ("
                + f.getName() + " y x))))";
        return ctx.parseSMTLIB2String(bench, new Symbol[] { t.getName() },
                new Sort[] { t }, new Symbol[] { f.getName() },
                new FuncDecl[] { f })[0];
    }

    // / "Hello world" example: create a Z3 logical context, and delete it.