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

还有怎么写这个

^{pr2}$

谢谢

Answer 1

您需要一个z3if-then-else，它可以用Z3中的If来定义。在

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

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

^{pr2}$

希望这有帮助。 This是从z3py开始的一个很好的资源。在