... | ... | @@ -97,16 +97,13 @@ b. 检查第 5 行和第 4 行: |
|
|
|
|
|
条件可以用布尔代数表示。如果行 `X` 是读操作(`is_write = 0`)且 `stack_pointer` 相同,则条件为真。我们用二进制变量表示条件:
|
|
|
|
|
|
$$
|
|
|
\text{condition} = (\text{is\_write}_X = 0) \times (\text{stack\_pointer}_X = \text{stack\_pointer}_{X-1})
|
|
|
$$
|
|
|
condition = (is_write_X = 0) * (stack_pointer_X = stack_pointer_{X-1})
|
|
|
|
|
|
|
|
|
写成表达式,需要将“行X若是读操作,上一行X-1如果和行X的stack pointer相同”写成一个二进制变量作为条件(`condition`),则约束表达式是:
|
|
|
|
|
|
$$
|
|
|
\text{condition} \times (value_X - value_{X-1}) = 0
|
|
|
$$
|
|
|
condition * (value_X - value_{X-1}) = 0
|
|
|
|
|
|
详细的如何写成`condition`,以及如何约束排序,详见state文档。
|
|
|
### Bytecode
|
|
|
|
... | ... | |