puzzel.py

from logic import *

AKnight = Symbol("A is a Knight")
AKnave = Symbol("A is a Knave")

BKnight = Symbol("B is a Knight")
BKnave = Symbol("B is a Knave")

CKnight = Symbol("C is a Knight")
CKnave = Symbol("C is a Knave")

Knight = Symbol("I am a Knight")
Knave = Symbol("I am a Knave")

# default game knowledge regarless of what is said
knowledge00 = And(
    Implication(AKnave, Not(Knave)),
    Implication(AKnave, Not(Knight)),  # a Knave always lies whatever he says

    Implication(AKnight, Knight),
    Implication(AKnight, Not(Knave)),  # a Knight always tells the truth

    # Each character is either a knight or a knave.
    Or(AKnave, AKnight),  # Inclusive "or" by implementation choice
    Not(And(AKnave, AKnight)),  # remove the inclusivity as cannot be both

    Or(BKnave, BKnight),
    Not(And(BKnave, BKnight)),

    Or(CKnave, CKnight),
    Not(And(CKnave, CKnight))
)

# Puzzle 0
# A says "I am both a knight and a knave."
knowledge0 = And(
    knowledge00,  # loads default game knowledge
    # add what the character actually said
    Implication(AKnave, Not(And(Knight, Knave))),
    Implication(AKnight, And(Knight, Knave))
)

# Puzzle 1

knowledge1 = And(
    knowledge00,

    # A says "We are both knaves."
    Implication(AKnight, And(AKnave, BKnave)),
    Implication(AKnave, Not(And(AKnave, BKnave)))

    # B says nothing.

)

# Puzzle 2
knowledge2 = And(
    knowledge00,

    # A says "We are the same kind."
    Implication(AKnight,
                Or(
                    And(AKnight, BKnight),
                    And(AKnave, BKnave)
                    )
                ),
    Implication(AKnave,
                And(
                    Not(And(AKnight, BKnight)),
                    Not(And(AKnave, BKnave))
                    )
                ),

    # B says "We are of different kinds."
    Implication(BKnight,
                Or(
                    And(AKnight, BKnave),
                    And(AKnave, BKnight)
                    )
                ),
    Implication(BKnave,
                And(
                    Not(And(AKnight, BKnave)),
                    Not(And(AKnave, BKnight))
                    )
                )
)

# Puzzle 3
knowledge3 = And(
    knowledge00,
    # A says either "I am a knight." or "I am a knave.", but you don't know which.
    Or(AKnight,AKnave),
    Not(And(AKnight,AKnave)),
    # B says "A said 'I am a knave'."
    Implication(BKnight, Biconditional(AKnave,Knave)),

    # B says "C is a knave."
    Implication(BKnight, CKnave),
    Implication(BKnave, Not(CKnave)),

    # C says "A is a knight."
    Implication(CKnight,AKnight),
    Implication(CKnave, Not(AKnight))

)


def main():
    symbols = [AKnight, AKnave, BKnight,
               BKnave, CKnight, CKnave, Knight, Knave]
    puzzles = [
        ("Puzzle 0", knowledge0),
        ("Puzzle 1", knowledge1),
        ("Puzzle 2", knowledge2),
        ("Puzzle 3", knowledge3)
    ]
    for puzzle, knowledge in puzzles:
        print(puzzle)
        if len(knowledge.conjuncts) == 0:
            print("    Not yet implemented.")
        else:
            for symbol in symbols:
                if model_check(knowledge, symbol):
                    print(f"    {symbol}")


if __name__ == "__main__":
    main()