mkOr(Expr<BoolSort> ...t) Z3 Java API 中的功能获取列表作为输入？

Question

不幸的是，我不能在这里发布整个代码，因为我在Java之上构建的DSL中编程(建模(。这个问题没有必要要求：

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

在python中，我现在可以将这个表达式列表提供给API的mkOr方法，就这样。不过，我下面的代码片段抱怨该列表不是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

可以，但它必须是一个正则数组；而不是CCD_ 1。因此，您应该首先将其转换为数组：

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函数。