z3 - 如何在 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 求解器不执行归纳，至少不是开箱即用的。你可以用很多辅助引理来哄他们这样做，并通过所谓的模式仔细引导；但这不是他们设计的，甚至不是他们擅长的。至少暂时不会。
有关相关问题的更多详细信息，请参阅此答案: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 和其他求解器对新语法有一定的支持，尽管它们无法真正证明这些函数的任何有趣属性。我怀疑社区的方向是最终某种程度的(用户引导的)归纳将成为这些求解器提供的工具箱的一部分，但目前情况并非如此。