Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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())
# initial_k.add(muddyB())
initial_k = Solver()
mA = Bool('mA')
mB = Bool('mB')
mC = Bool('mC')
initial_k.add(Or(Or(mA, mB), mC))
print initial_k.check()
print initial_k.model()
# So now there are two alternatives: mA can be True or False
# Note that this is implicit in the output model!
# Now we get the following announcements:
# * Not(Kb[mB])
# * Not(Kc[mC])
# Let's iterate over possibilities for mA and knowledge
# results
w_results = {}
# We know that mB, Not(mC)
for wA in [mA, Not(mA)]:
initial_k.push()
initial_k.add(wA)
def check_assumption(fact, solver):
solver.push()
solver.add(fact)
res = solver.check()
model = None
if res == sat:
model = solver.model()
solver.pop()
return (res, model)
# We know that And(Not(Kb[mB]), Not(Kb[Not(mB)]))
# This implies that the possible models
# under each assumption are not homogeneous
initial_k.add(Not(mC))
models_b = {wB: check_assumption(wB, initial_k) for wB in [mB, Not(mB)]}
# models are
possibles = [model.eval(mB) for (is_mb, (res, model)) in models_b.items() if model]
# print "[{0} {1}] => {2}".format(wA, wB, (res, model))
print possibles
initial_k.pop()
if all(possibles) or not any(possibles):
# Assuming wA, then we violate the knowledge of B
# assumptions! therefore, wA cannot be valid
print "{0} means Kb[mB = {1}]".format(wA, possibles[0])
else:
print "And(Not(Kb[mB]), Not(Kb[Not(mB)]))"
print str(datetime.now())
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment