Z3 Python API 中的扩展欧几里得算法答案

【问题标题】：Extended Euclidean Algorithm in Z3 Python APIZ3 Python API 中的扩展欧几里得算法
【发布时间】：2021-07-26 01:38:05
【问题描述】：

我试图在 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()

【问题讨论】：

好吧，你的函数无条件地调用自己，所以它有无限递归。你真的需要对这个算法的过程进行建模，还是只需要表示两个整数互质的约束？
谢谢。我需要对这个算法的过程进行建模。如果 b == 0，则递归应该停止，这是在 Python 中运行良好的第一个函数的情况 - 假设递归的深度设置正确。
b 是一个形式变量，在您调用函数时它不能等于零，因为它当时没有值。而且你的函数无条件地调用自己，If 实际上并没有在这里分支。

标签： python z3 smt

【解决方案1】：

这里的问题是您正在使用符号输入运行函数，因此递归永远不会停止。您不能直接使用 Python 函数对这样的递归函数进行建模，除非您保证递归将具体停止。

一个经典的技巧是向函数传递一个额外的计数器，它将是一个常规整数（不是 z3 符号整数！），在每次递归调用中都会递减。只要计数足够大，您就可以通过这种方式完成验证。但是确定计数应该有多大取决于您要建模的算法，并且可能很难确定。

另一种选择是使用 z3 的递归函数定义功能，您可以将函数递归地编写为 z3py 函数（不是 Python 函数）。然而，这也相当棘手，因为大多数递归函数都需要归纳证明，而 SMT 求解器不进行归纳。

总而言之，z3（或任何其他 SMT 求解器）并不是真正适合对此类递归程序进行建模的工具。相反，请使用适当的定理证明器，例如 Isabelle、ACL2、Coq、Lean 等；所有这些都支持这种开箱即用的递归定义。虽然这些工具不是按钮式的，但它们提供了大量的自动化证明来帮助您。

【讨论】：

非常感谢您的 cmets。