如何在 Z3 中表示符号求和？

Question

我正在尝试表示从整数 a 到形式

的整数 b 的整数总和

\sum_{i=a}^b i

当然，这个版本有一个封闭形式的解决方案，但总的来说，我想对 i 参数化的表达式求和。我目前尝试定义一个函数 symSum 并使用通用量词描述其行为：

from z3 import *
s = Solver()
symSum = Function('symSum', IntSort(), IntSort(), IntSort())

a = Int('a')
b = Int('b')
s.add(ForAll([a,b],If(a > b,symSum(a,b) == 0,symSum(a,b) == a + symSum(a+1,b))))
x = Int('x')
s.add(x == symSum(1,5))
print(s.check())
print(s.model())

我还没有让这段代码终止（不过我最多只允许它运行几分钟）。这超出了 Z3 的能力范围吗？

编辑： 仔细研究一下，我能够使用递归函数来定义它！

from z3 import *
ctx = Context()
symSum = RecFunction('symSum', IntSort(ctx), IntSort(ctx), IntSort(ctx))
a = Int('a',ctx)
b = Int('b',ctx)
RecAddDefinition(symSum, [a,b], If(a > b, 0, a + symSum(a+1,b)))
x = Int('x',ctx)

s = Solver(ctx=ctx)
s.add(symSum(1,5) == x)
print(s.check())
print(s.model())

Answer 1

是；这超出了 SMT 求解器的当前能力。

想象一下您将如何亲手证明这样的事情。你必须对自然数进行归纳。 SMT 求解器不执行归纳，至少不是开箱即用的。您可以通过大量辅助引理并通过所谓的模式进行仔细指导来哄骗他们这样做；但这不是他们设计的，甚至不擅长的。至少暂时不会。

有关相关问题的更多详细信息，请参阅此答案：

话虽如此，最新版本的 SMTLib 确实包含定义递归函数的功能。（请参阅 https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf，第 4.2.3 节。）z3 和其他求解器对新语法有一些支持，尽管它们无法真正证明这些函数的任何有趣属性。我怀疑社区的方向是最终某种程度的（用户引导的）归纳将成为这些求解器提供的工具箱的一部分，但目前情况暂时并非如此。

如何在 Z3 中表示符号求和？

How to represent a symbolic summation in Z3?

z3

smt

z3py