Mobile Phone Feature Model for Z3 (in Python)

from z3 import *

# All features are declared as Boolean variables
Mobile_Phone = Bool('Mobile_Phone')
Calls = Bool('Calls')
Screen = Bool('Screen')
GPS = Bool('GPS')
Media = Bool('Media')
Basic = Bool('Basic')
Color = Bool('Color')
High_res = Bool('High_res')
Camera = Bool('Camera')
MP3 = Bool('MP3')

s = Solver()

# Mandatory features; double implication
s.add( Mobile_Phone == Calls )
s.add( Mobile_Phone == Screen )

# Optional features; child implies parent
s.add( Implies (GPS,Mobile_Phone) )
s.add( Implies (Media,Mobile_Phone) )
s.add( Implies (Basic,Screen) )
s.add( Implies (Color,Screen) )
s.add( Implies (High_res,Screen) )
s.add( Implies (Camera,Media) )
s.add( Implies (MP3,Media) )

# [1,1] group
s.add( Or ( And(Basic,Not(Color),Not(High_res)) ,
And(Not(Basic),Color,Not(High_res)) ,
And(Not(Basic),Not(Color),High_res) ) )

# [1,*] group
s.add( Or (Camera,MP3) )

print s.check()
print s.model()