如何在 Z3 java API 中定义一个函数？答案

【问题标题】：How to define a function in Z3 java API?如何在 Z3 java API 中定义一个函数？
【发布时间】：2020-12-18 00:17:49
【问题描述】：

我正在学习在匹配案例中运行类似的代码，用于在 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), a, b);

我对用JAVA 构建z3 函数肯定有疑问。 Z3 Java API 是否存在特殊的函数形式？如何修复该功能？

【问题讨论】：

标签： java optimization z3

【解决方案1】：

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

【讨论】：