如何在 z3py 中声明一个自然数变量？

【问题标题】：How to declare a natural number variable in z3py?如何在 z3py 中声明一个自然数变量？
【发布时间】：2022-08-08 10:54:01
【问题描述】：

我想在我的约束中推理自然数。

我知道我可以做类似的事情：

x = Int(\'x\') 然后添加一个约束 x >= 0。但是有没有更好的方法来做到这一点，这样我就不必每次声明变量时都添加额外的约束？

标签： python z3 smt z3py

【解决方案1】：

不幸的是，没有“好”的方式来模拟自然。您最好的选择是根据需要添加>= 0 约束。请注意，您需要在每次数学运算之后执行此操作，尤其是减法。

如果机器算术是可以接受的（例如，对某些 n 取模 2^n；通常是 n=32 或 n=64），那么位向量就更远了。请注意，在 SMTLib 中，位向量是无符号的，只有操作是无符号的。因此，您无需一直添加>= 0 形式的额外约束即可逃脱。请参阅Is there an UnsignedIntSort in Z3? 进行讨论。

【讨论】：