Method injAxiomAbs

examples/java/JavaExample.java:104–148

(Context ctx, FuncDecl f, int i)

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

    public BoolExpr injAxiomAbs(Context ctx, FuncDecl 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 */
        Sort finv_domain = f.getRange();
        Sort finv_range = domain[i];
        FuncDecl finv = ctx.mkFuncDecl("f_fresh", finv_domain, finv_range);

        /* allocate temporary arrays */
        Expr[] xs = new Expr[sz];

        /* fill types, names and xs */
        for (int j = 0; j < sz; j++)
        {
            xs[j] = ctx.mkConst("x_" + Integer.toString(j), domain[j]);
        }
        Expr x_i = xs[i];

        /* create f(x_0, ..., x_i, ..., x_{n-1}) */
        Expr fxs = f.apply(xs);

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

        /* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */
        Expr 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 */
        BoolExpr q = ctx.mkForall(xs, /* types of quantified variables */
                eq, /* names of quantified variables */
                1, new Pattern[] { p } /* patterns */, null, null, null);

        return q;
    }

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