Skip to content

Instantly share code, notes, and snippets.

Avatar

javiermtorres

View GitHub Profile
View muddy.py
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())
View agent.py
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