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