如何在 Z3py 中定义分段函数

Question

我想在 Z3py 中定义一个分段（线性）函数，例如函数f(x) 的形式为

f(x) = a*x + b when 0 <= x <= 1
f(x) = exp(c*x) when 1 < x <= 2
f(x) = 1/(1+10^x) when 2 < x <= 3
etc.

其中a、b 和c 是常量。

我猜z3.If() 函数是相关的，但是随着片段数量的增加，表达式变得复杂。

我的问题是，Z3py 是否提供了 if-else 语句，或者是否有一种优雅的方式在 Z3py 中定义分段函数？

Answer 1

是的，Z3 支持 if-then-elses，在 Python 中可以使用 If 函数构造它们。 If文档中的一个例子：

>>> x = Int('x')
>>> y = Int('y')
>>> max = If(x > y, x, y)
max = If(x > y, x, y)