python - 在 Z3 Python API 中使用布尔 If 重新初始化实变量

Question

我需要根据一些布尔标志重新初始化一个实变量，如下所示。除了改变location_next我想x_next用另一个值重新初始化的真值。我怎样才能做到这一点？

location, location_next = Bools('location location_next')
x, x_next = Reals('x x_next')
...
location_next == If(And(Not(location), x_next >= 12),
                    True,
                    If(And(location, x_next <= 0), False, location))

Answer 1

该函数If（在 Z3 API 中）也可用于创建非布尔表达式。我们必须为每个If(c, t1, t2),c具有排序布尔值，t1并且t2具有相同的排序 (类型) S。在这种情况下，If(c, t1, t2)is 将生成 sort 的 Z3 表达式S。这是一个小例子：

x, y = Reals('x y')
print If(x > 0, x + 1, y - 1)

这是上面示例的链接：http ://rise4fun.com/Z3Py/V4e

在下面的示例中，我们有一个公式，x_next它等于x+1when locationis Falseand x >= 12，等于x-1when locationis Trueand x <= 0，并且等于xelse 。

x_next == If(And(Not(location), x >= 12),
             x+1,
             If(And(location, x <= 0), x-1, x))