python - Z3 Python API 中的扩展欧几里得算法
问题描述
我试图在 Z3 中对扩展的欧几里得算法进行建模,但遇到了无限循环。
欢迎提出建议和意见。
第一个函数是用 Python 编写的 - 仅供参考。
第二个函数是在 z3 分析时陷入无限循环的函数。
您是否发现我如何将常规 Python 函数映射到相应的 Z3 语法有任何错误?
'''
Returns d, x, y such that a*x + b*y = d
d = gcd(a, b)
'''
def extended_euclid_rec(a, b):
if b == 0:
d = a; x = 1; y = 0 # y can be any int
return d, x, y
else:
d, x1, y1 = extended_euclid_rec(b, a % b)
q = a // b
x = y1
y = x1-y1*q
assert a*x + b*y == d
return d, x, y
此函数进入无限循环。
def extended_euclid(a, b):
d = If(b == 0, a, extended_euclid(b, a % b)[0])
x1 = If(b == 0, 1, extended_euclid(b, a % b)[1])
y1 = If(b == 0, 0, extended_euclid(b, a % b)[2])
q = If(b == 0, 1, a // b)
x = If(b == 0, 1, y1)
y = If(b == 0, 0, x1-y1*q)
return d, x, y
a = Int('a')
b = Int('b')
s = Solver()
s.add(extended_euclid(a, b)[0] == 1)
print s.sexpr()
print s.check()
解决方案
这里的问题是您正在使用符号输入运行函数,因此递归永远不会停止。您不能直接使用 Python 函数对这样的递归函数进行建模,除非您保证递归将具体停止。
一个经典的技巧是向函数传递一个额外的计数器,它将是一个常规整数(不是 z3 符号整数!),在每次递归调用中都会递减。只要计数足够大,您就可以通过这种方式完成验证。但是确定计数应该有多大取决于您要建模的算法,并且可能很难确定。
另一种选择是使用 z3 的递归函数定义功能,您可以将函数递归地编写为 z3py 函数(而不是 Python 函数)。然而,这也相当棘手,因为大多数递归函数都需要归纳证明,而 SMT 求解器不进行归纳。
总而言之,z3(或任何其他 SMT 求解器)并不是真正适合对此类递归程序进行建模的工具。相反,请使用适当的定理证明器,例如 Isabelle、ACL2、Coq、Lean 等;所有这些都支持这种开箱即用的递归定义。虽然这些工具不是按钮式的,但它们提供了大量的自动化证明来帮助您。
推荐阅读
- php - 如何对多维数组进行分组和回显
- unity3d - 有没有办法将此 Unity 2d 代码分解为单独的方法
- android - 我的 webview 没有出现在我的 android 应用程序中,但没有错误
- qt - Qt 和 Qss:如何使滑块框中的文本和非标签文本更大?
- keras - tf.keras.layers.Conv2D() 不适用于将 Keras 后端设置为 float16
- excel - 如何在一列中查找多个起始字母?
- handlebars.js - 车把 - 这种语法有效吗?
- powerbi - Power BI Report 衡量按时完成的作业
- regex - 用于从 Dataframe 中删除空格的 RegEx
- javascript - 如何通过 JavaScript 设置 PHP 变量以隐藏特定视口宽度的图像