Z3 Java Api 中的 mkOr(Expr<BoolSort> ... t) 函数可以获取列表作为输入吗？

Question

不幸的是，我无法在此处发布整个代码，因为我正在使用基于 Java 构建的 DSL 进行编程（建模）。不过，这个问题并不一定要求：

我正在尝试创建更长的 Or-Expression，例如：p == 1 或 p==2 或 p==3 等等。 我有一个 BoolExpr 列表，其中包含那些 EQ 表达式（即 p==1 等）的列表。

在 python 中，我现在可以将这个表达式列表提供给 API 的 mkOr 方法，就是这样。我下面的代码 sn-p 虽然抱怨列表不是 BoolExpr 的子类型。

list<BoolExpr> eqExprList = new arraylist<BoolExpr>;

// populate this list with p==1, p==2 etc.

MyContext.mkOr(eqExrList); // this produces the error

所以问题基本上是，它是否应该正常（在真正的 java 中）这样工作，或者我是否误解了 API 文档：https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_context.html#aea714fc46f4c625ecc15397522099330

Answer 1

是的，你可以，但它必须是一个常规数组；不是ArrayList。所以，你应该先把它转换成一个数组：

import com.microsoft.z3.*;
import java.util.*;

public class Z3Test {

  public static void main(String[] args) {
      Context ctx = new Context();

      IntExpr x = ctx.mkIntConst("x");
      IntExpr y = ctx.mkIntConst("y");
      IntExpr z = ctx.mkIntConst("z");

      ArrayList<BoolExpr> eqExprList = new ArrayList<BoolExpr>();
      eqExprList.add(ctx.mkEq(x, y));
      eqExprList.add(ctx.mkEq(y, z));

      Solver s = ctx.mkSolver();
      s.add(ctx.mkOr(eqExprList.toArray(new BoolExpr[eqExprList.size()])));

      System.out.println(s);
  }
}

打印出来：

(declare-fun z () Int)
(declare-fun y () Int)
(declare-fun x () Int)
(assert (or (= x y) (= y z)))

所以你缺少的部分是：

ctx.mkOr(eqExprList.toArray(new BoolExpr[eqExprList.size()]))

从ArrayList 中创建一个常规数组，然后可以将其馈送到mkOr 函数。