如何在 Z3 Java API 中定义带约束的递归函数？

Question

我正在使用 Z3 Java API 并尝试通过使用递归 API 定义函数 f(x) = x + 1。但是，我不想直接将函数定义为 y = x + 1，而是想使用约束来表示这种关系。下面是我写的代码：

    @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
    }

该函数未按预期运行。约束 f(1) != 2 应该是不可满足的，但似乎约束没有正确应用。

如何使用 Z3 Java API 中的约束正确定义函数 f(x) = x + 1？

Answer 1

一般来说，定义函数时，只需返回定义表达式即可。 （即，不要返回带有约束的“自由”变量；只需构建表达式本身。）

所以，你应该写：

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());
    }
}

当我运行这个时，我得到：

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

所以，您确实得到了

UNSATISFIABLE

正如您所期望的那样。我没有在这里检查

unchecked-unsafe

操作的来源，这可能是一个好主意，可以考虑额外的安全性。