How to Define a Recursive Function with Constraints in Z3 Java API?

I am working with the Z3 Java API and trying to define a function f(x) = x + 1 via using recursive API. However, instead of directly defining the function as y = x + 1, I want to use constraints to represent this relationship. Below is the code I have written:

    @Test
    public void test1() {
        Context ctx = new Context();
        FuncDecl f = ctx.mkRecFuncDecl(ctx.mkSymbol("f"),
                new Sort[]{ctx.mkIntSort()},
                ctx.mkIntSort());
        Expr x = ctx.mkFreshConst("x", ctx.mkIntSort());
        Expr y = ctx.mkFreshConst("y", ctx.mkIntSort());
        Expr cons = ctx.mkEq(ctx.mkAdd(x, ctx.mkInt(1)), y);
        ctx.AddRecDef(f, new Expr[]{x}, y);
        Solver solver = ctx.mkSolver();
        solver.add(cons);

        solver.add(ctx.mkNot(ctx.mkEq(ctx.mkInt(2), ctx.mkApp(f, ctx.mkInt(1)))));

        assert solver.check() == Status.UNSATISFIABLE; //Fail
    }

the function does not behave as expected. The constraint f(1) != 2 should be unsatisfiable, but it seems like the constraints are not correctly applied.

How can I correctly define function f(x) = x + 1 using constraints in the Z3 Java API?

Solution

In general, when you're defining a function, simply return the defining expression. (i.e., do not return a "free" variable with constraints on it; simply build the expression itself.)

So, you should write:

import com.microsoft.z3.*;

class Test {
    public static void main(String[] args) {
        Context ctx = new Context();
        FuncDecl f = ctx.mkRecFuncDecl(ctx.mkSymbol("f"),
                new Sort[]{ctx.mkIntSort()},
                ctx.mkIntSort());
        Expr x = ctx.mkFreshConst("x", ctx.mkIntSort());
        ctx.AddRecDef(f, new Expr[]{x}, ctx.mkAdd(x, ctx.mkInt(1)));
        Solver solver = ctx.mkSolver();
        solver.add(ctx.mkNot(ctx.mkEq(ctx.mkInt(2), ctx.mkApp(f, ctx.mkInt(1)))));

        System.out.println(solver.check());
    }
}

When I run this, I get:

Note: Test.java uses unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
UNSATISFIABLE

So, you do get UNSATISFIABLE as you'd expect. I didn't inspect the source of unchecked-unsafe operations here, which is probably a good idea to look at for additional safety.