python - z3py 中的 if 断言

Question

我是 z3py 的新用户。我需要编写一个程序来检查某些规则的满足情况，例如

IF room.temp < 18 THEN room.fireplace = on  
IF room.temp > 24 THEN room.fireplace = off  
IF room.CO > 180  THEN room.fireplace = off  
IF room.temp > 28 THEN house.hvac = off  
IF house.hvac == on THEN room.fireplace = off

还有如何写这个

bedroom.occupancy  ==  true  and  bedroom.env_brightness  <=  31.5 and  bedroom.light.switch = on

谢谢

Answer 1

您需要一个 Z3 If-then-else，可以使用 z3 中的 If 进行定义。

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

要定义多个约束，您可以使用 And 和 Or

>>> max = If(And(x>y, x!=0), x, y)
>>> max
If(And(x > y, x != 0), x, y)
>>> simplify(max)
If(And(Not(x <= y), Not(x == 0)), x, y)

希望这有帮助。 This一般来说，这是开始使用 z3py 的一个很好的资源。