如果在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開始。