Method commAxiom

examples/java/JavaGenericExample.java:147–162

(Context ctx, FuncDecl<R> f)

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

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

        String bench = String.format("(assert (forall (x %s) (y %s) (= (%s x y) (%s y x))))", t.getName(), t.getName(), f.getName(), f.getName());
        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.