Knights

knights.py

#!/usr/bin/env python3

from z3 import *

Person = Datatype("Person")
Person.declare("knight")
Person.declare("knave")
Person.declare("joker")
Person = Person.create()

ellis = Const("ellis", Person)
farin = Const("farin", Person)
gobi = Const("gobi", Person)

def calls_joker(a, b):
    return Or(
        # Jocker can call anyone a jocker
        a == Person.joker,
        # Knight tells truth
        And(a == Person.knight, b == Person.joker),
        # Knave tells lies
        And(a == Person.knave, b != Person.joker),
    )

s = Solver()
# Exactly one joker
s.add(Sum([If(p == Person.joker, 1, 0) for p in [ellis, farin, gobi]]) == 1)
# Who calls whom a jocker
s.add(calls_joker(ellis, farin))
s.add(calls_joker(farin, gobi))
s.add(calls_joker(gobi, ellis))

while s.check() == sat:
    # Print the solution
    print(s.model())
    # And then block this solution to find next solution
    block = []
    for var in s.model():
        const = var()
        block += [s.model()[var] == const]
    s.add(Not(And(block)))

# vim: set ts=4 sw=4 et: