アサーションが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 

のようないくつかのルールの満足度をチェックするプログラムを記述する必要はまたあなたが定義することができZ3-THEN-ELSEの場合に必要なこの

bedroom.occupancy == true and bedroom.env_brightness <= 31.5 and bedroom.light.switch = on 

おかげ

Answer 1

を作成する方法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から始めるのに最適なリソースです。