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())
# 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())