我是 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
谢谢
最佳答案
您需要一个 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 的一个很好的资源。
关于python - z3py 中的 if 断言,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/41148228/