CODEWITHSUNDEEP
z3smt
Ajit
Ajit

Reputation: 31

Error adding containts to solver in z3

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

For the above assign statement which is in verilog, i getting error while implememting it in z3

My code: 

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]));

I am getting error in above add statement: error: method mkBVAND in class Context cannot be applied to given types; required: BitVecExpr,BitVecExpr found: BitVecExpr,BoolExpr

Which is true. Can anyone suggest me workaround. Am i implementing it incorrectly please let me know.

Upvotes: 1

Views: 79

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8402

This error is reported because the second argument of mkBVAND is a Boolean expression (ctx.mkEq ...). Note that Booleans and BitVectors of size 1 are not the same thing, and they will not be converted automatically. The easiest way to convert between them is an if-then-else the selects the right values.

These are the problems with this example:

1) ctx.mkNumeral("2",2) is incorrect. I guess the intention was to create a bv-numeral of 2 bits with value 2; the easiest way to achieve that is ctx.mkBV(2, 2)

2) The 2nd argument of mkBVAND needs to be converted from Bool to BitVector, e.g., like so:

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 being the result.

3) ctx.mkBVAND takes exactly 2 arguments, no more and no less. Thus, the BVAND expression needs to be rewritten, e.g., like so:

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

4) The result needs to be converted to a Boolean expression again, e.g.

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

where q is the result of the BVAND.

Upvotes: 1

Related Questions