Method injAxiomAbs

examples/java/JavaGenericExample.java:101–139

(Context ctx, FuncDecl<R> f, int i)

    // / Where, <code>finv</code>is a fresh function declaration.

    public <R extends Sort> BoolExpr injAxiomAbs(Context ctx, FuncDecl<R> f, int i)
    {
        Sort[] domain = f.getDomain();
        int sz = f.getDomainSize();

        if (i >= sz)
        {
            System.out.println("failed to create inj axiom");
            return null;
        }

        /* declare the i-th inverse of f: finv */
        R finv_domain = f.getRange();
        Sort finv_range = domain[i];
        FuncDecl<Sort> finv = ctx.mkFuncDecl("f_fresh", finv_domain, finv_range);

        /* allocate temporary arrays */
        List<Expr<Sort>> xs = IntStream.range(0, sz).mapToObj(j -> ctx.mkConst(String.format("x_%d", j), domain[j])).collect(Collectors.toList());

        /* fill types, names and xs */
        Expr<Sort> x_i = xs.get(i);

        /* create f(x_0, ..., x_i, ..., x_{n-1}) */
        Expr<R> fxs = f.apply(xs.toArray(new Expr[0]));

        /* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */
        Expr<Sort> finv_fxs = finv.apply(fxs);

        /* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */
        BoolExpr eq = ctx.mkEq(finv_fxs, x_i);

        /* use f(x_0, ..., x_i, ..., x_{n-1}) as the pattern for the quantifier */
        Pattern p = ctx.mkPattern(fxs);

        /* create & assert quantifier */
        return ctx.mkForall(xs.toArray(new Expr[0]), /* types of quantified variables */
                eq, /* names of quantified variables */
                1, new Pattern[] { p } /* patterns */, null, null, null);
    }

    // / Assert the axiom: function f is commutative.