如果在z3py中声明

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开始。