... | ... | @@ -77,8 +77,8 @@ operand* 用来存放算术中的参数值,如 a+b=c+overflow 指令中的 a,b |
|
|
我们有(a-d)/b = c ==> c * b + d = a 同时约束 d 小于 b
|
|
|
```
|
|
|
|
|
|
if tag is div, (a,b,c,d) = (pop1,pop2,push,pop1 - push * pop2) (push, pop2, pop1 - push \* pop2, pop1)
|
|
|
if tag is mod, (a,b,c,d) = (pop1 ,pop2 , if pop2 is zero{zero}else{pop1 / pop2} ,if pop2 is zero{zero}else{push})
|
|
|
if tag is div, (a,b,c,d) = (pop1,pop2,push,pop1 - push * pop2)
|
|
|
if tag is mod, (a,b,c,d) = (pop1 ,pop2 , if pop2 is zero{zero}else{pop1 / pop2} ,if pop2 is zero{pop1}else{push})
|
|
|
|
|
|
define
|
|
|
a * b + c = d
|
... | ... | |