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)

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