在 z3 中向求解器添加约束时出错

Question

assign wfwe = wb_acc & (adr_i == 2'b10) & ack_o &  we_i;

对于上述在verilog中的assign语句，我在z3中实现它时出错

我的代码：

BitVecExpr[] wfwe = new BitVecExpr[1];
BitVecExpr[] wb_acc = new BitVecExpr[1];
BitVecExpr[] adr_i = new BitVecExpr[1];
BitVecExpr[] ack_o = new BitVecExpr[1];
BitVecExpr[] we_i = new BitVecExpr[1];

wfwe[0] = ctx.mkBVConst("wfwe",1);
wb_acc[0] = ctx.mkBVConst("wb_acc",1);
adr_i[0] = ctx.mkBVConst("adr_i",2);
ack_o[0] = ctx.mkBVConst("ack_o",1);
we_i[0] = ctx.mkBVConst("we_i",1);

Solver s = ctx.mkSolver();

s.add(ctx.mkBVAND(wb_acc[0],ctx.mkEq(adr_i[0],ctx.mkNumeral("2",2)),ack_o[0],we_i[0]));

我在上面的 add 语句中遇到错误： 错误：类 Context 中的方法 mkBVAND 不能应用于给定类型； 必需：BitVecExpr,BitVecExpr 找到：BitVecExpr,BoolExpr

这是真的。任何人都可以建议我解决方法。我是否执行不正确，请告诉我。

Answer 1

报告此错误是因为 mkBVAND 的第二个参数是布尔表达式 (ctx.mkEq ...)。请注意，布尔值和大小为 1 的 BitVector 不是一回事，它们不会自动转换。在它们之间进行转换的最简单方法是 if-then-else 选择正确的值。

这些是这个例子的问题：

1) ctx.mkNumeral("2",2) 不正确。我想目的是创建一个值为 2 的 2 位 bv 数字；实现这一目标的最简单方法是ctx.mkBV(2, 2)

2) mkBVAND 的第二个参数需要从 Bool 转换为 BitVector，例如，像这样：

BoolExpr c = ctx.mkEq(adr_i[0], ctx.mkBV(2, 2));
BitVecExpr e = (BitVecExpr) ctx.mkITE(c, ctx.mkBV(1, 1), ctx.mkBV(0, 1));

e 是结果。

3) ctx.mkBVAND 正好有 2 个参数，不多也不少。因此，需要重写 BVAND 表达式，例如：

ctx.mkBVAND(ctx.mkBVAND(wb_acc[0], e), ctx.mkBVAND(ack_o[0], we_i[0])))

4) 结果需要再次转换为布尔表达式，例如

ctx.mkEq(q, ctx.mkBV(1, 1))

q 是 BVAND 的结果。