CODEWITHSUNDEEP
z3smt
Ajit
Ajit

Reputation: 31

Assign value to specific bit of BitVecExpr in Z3

Here is my verilog statement:

reg[2:0] a;            // Create register 'a' which is 3 bit.
assign a[1] = 1'b1;    // Assigning value to 1st bit of register 'a'.

I have to implement the statement above in Z3. For the 1st line of the verilog statement using BitVecExpr:

BitVecExpr a = ctx.mkBVConst("a",3);

I am a facing problem while implementing 2nd line of verilog statement. Does anyone know how to implement this in Z3?

Upvotes: 1

Views: 207

Answers (1)

usr
usr

Reputation: 171236

With Z3 you can't modify variables. In fact Z3 doesn't call this a variable, it's a constant.

You need to make a new constant that is related to the old constant. For example if you want to say y = x + 1 this would be

var y = ctx.MkBVAdd(x, 1);

If you want to say x = x + 1 you need to introduce a new name for the old and for the new x:

var x2 = ctx.MkBVAdd(x1, 1);

Upvotes: 1

Related Questions