javiermtorres

from z3 import *
from datetime import datetime

print str(datetime.now())
# initial_k = Solver()
# muddyA = Function('muddyA', BoolSort())
# muddyB = Function('muddyB', BoolSort())
# muddyC = Function('muddyC', BoolSort())
# initial_k.add(muddyA())

javiermtorres

from z3 import *

s = Solver()
Room, (roomA, roomB) = EnumSort('Room', ['roomA', 'roomB'])
Key, (goldKey, brassKey) = EnumSort('Key', ['goldKey', 'brassKey'])
in_room = Function('in_room', Key, Room, BoolSort())
r = Const('r', Room)
print r
r1 = Const('r1', Room)
print r1