Z3 求解器的位数

Question

我可以在 Z3py 求解器上指定 Int 中的位数吗？例如，X > 1 但 X 有 3 个数字 ( 111 > 1) 我可以确定模型将 return 的数字位数吗？

换句话说：我想根据我给定的长度生成数字。例如，我给定 length = 3，我希望求解器生成 3 位数字

Answer 1

您可以使用 Length 和 IntToStr 方法：

from z3 import *

x = Int('x')
l = Int('l')

s = Solver()
s.add(Length(IntToStr(x)) == l)

# make it interesting
s.add(l > 3)

print(s.check())
print(s.model())

这会打印：

sat
[x = 1400, l = 4]

请注意，如果对整数和长度的约束很复杂，IntToStr 方法不太可能有效（即，您可能会得到未知数或可能太长而无法计算）。如果长度是一个固定的常数，它应该表现良好。

Answer 2

我建议您根据所需长度将 X 限制在特定范围内。如果您希望 X 有 L 个数字，请使用

And(X >= 10**(L-1), X < 10**L)

我希望这比转换为字符串然后尝试对字符串应用约束更好。

Z3 求解器的位数

Number of digits on Z3 Solver

integer

z3

z3py