if assertion in z3py

Question

i'm a new user for z3py. I need to write a program that check satisfaction of some rule like

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

also how to write this

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

thanks

Answer 1

You need a Z3 If-then-else which can be defined using If in z3.

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

For defining multiple constraints you can use And 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)

Hope this helps. This is a great resource to start with z3py in general.