Присвоить значение определенному биту BitVecExpr в Z3

Вот мое утверждение 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. Для 1-й строки оператора Verilog с использованием BitVecExpr:

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

Я столкнулся с проблемой при реализации 2-й строки оператора Verilog. Кто-нибудь знает, как это реализовать в Z3?


z3 smt
person Ajit    schedule 14.08.2015    source источник
comment
@ChristophWintersteiger Как вы думаете, у нас есть прямое решение этой проблемы в Z3?   -  person Ajit    schedule 18.08.2015

Ответы (1)


arrow_upward
1
arrow_downward

В Z3 вы не можете изменять переменные. На самом деле Z3 не называет это переменной, это константа.

Вам нужно создать новую константу, связанную со старой константой. Например, если вы хотите сказать y = x + 1, это будет

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

Если вы хотите сказать x = x + 1, вам нужно ввести новое имя для старого и для нового x:

var x2 = ctx.MkBVAdd(x1, 1);
person usr    schedule 14.08.2015
comment
Я понимаю, что вы хотели сказать, но моя проблема в том, что у меня есть несколько назначений для одной константы. Например: назначьте a[1] = 1'b1; присвоить a[0] = 1'b0; присвоить a[3:2] = 2'b01; и так далее. Я думал, есть ли какое-либо прямое решение этой проблемы, например, я могу напрямую присвоить значение любому конкретному биту в Z3. Как вы думаете, мы можем это сделать? - person Ajit; 18.08.2015
comment
Присвоение значений не имеет смысла. Вы просите Z3 дать вам модель булевой формулы. Вы не можете назначать части формулы. Вероятно, вам нужно что-то вроде b = replacebits(ctx, a), где replacebits обозначает такие операции, как MkExtract или MkConcat. - person usr; 19.08.2015