值分配給在Z3

Question

BitVecExpr的特定位這是我的Verilog聲明：

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

我要實現上述Z3的聲明。 對於使用BitVecExpr Verilog的語句的第一行：

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

我是一個面臨的問題而實施的Verilog聲明第二條線。 有誰知道如何在Z3中實現這個？

Answer 1

使用Z3不能修改變量。實際上Z3並不把它稱爲變量，而是一個常量。

您需要創建一個與舊常數相關的新常量。例如，如果你想說y = x + 1，這將是

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

如果你想說x = x + 1你需要舊和新x引入一個新的名字：

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