如何在Z3 Java API中定义函数？

问题描述

我正在学习在匹配的情况下运行类似的代码，该代码用于匹配JAVA API中用于运输的卡车（https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf）。有一个用于定义max函数的代码：

(define-fun imax ((a Int) (b Int)) Int (if (> a b) a b))

我将其翻译为Java：

     public static ArithExpr maxFunc(ArithExpr a,ArithExpr b)
     {
         Context ctx = new Context();
         ArithExpr result = (ArithExpr) ctx.mkITE(ctx.mkGe(a,b),a,b);
         return result;
     }

并尝试以相同的方式使用它（以下只是一个演示）

        ArithExpr per1 = maxFunc(X0101,maxFunc(X0201,maxFunc(X0301,maxFunc(X0401,X0501))));
        BoolExpr minPer1 = ctx.mkEq(per1,constant0);
        o.AssertSoft(minPer1,1,"a");

以上代码有误：

Exception in thread "main" com.microsoft.z3.Z3Exception: Context mismatch

错误涉及函数体：

ArithExpr result = (ArithExpr) ctx.mkITE(ctx.mkGe(a,b);

我绝对怀疑在JAVA中构造z3函数。 Z3 Java API是否存在特殊功能形式？如何修复该功能？

解决方法

“上下文不匹配”表示您正在尝试同时使用多个上下文中的表达式，这不受支持。请确保使用与程序其余部分相同的上下文，而不是Context ctx = new Context();。

java java optimization z3