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

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

我试图表示从整数 a 到整数 b 形式的整数之和

\sum_{i=a}^b i

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

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

a = Int('a')
b = Int('b')
s.add(ForAll([a,b],If(a > b,symSum(a,b) == 0,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))
a = Int('a',ctx)
b = Int('b',ctx)
RecAddDeFinition(symSum,[a,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())

解决方法

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

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

有关相关问题的更多详细信息，请参阅此答案：Is it possible to prove this defined function is an involution in z3?

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