在z3中向求解器添加包含时出错

Question

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

对于上面的赋值语句，在verilog中，在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]));

我在上面的添加语句中得到错误:错误:类Context中的mkBVAND方法不能应用于给定的类型;要求:BitVecExpr BitVecExpr发现:BitVecExpr BoolExpr

这是真的。谁能给我提个建议。我执行它不正确，请让我知道。

Answer 1

报告此错误，因为mkBVAND的第二个参数是布尔表达式(ctx)。mkEq……)。请注意，布尔值和大小为1的比特向量不是一回事，它们不会被自动转换。在它们之间进行转换的最简单方法是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的结果