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")

# Puzzle 0
# A says "I am both a knight and a knave."
knowledge0 = And(
    # knight or knave, only one
    Or(And(AKnight, Not(AKnave)), And(AKnave, Not(AKnight))),
    # if knight and knave compute true then a is knight
    Biconditional(And(AKnight, AKnave), AKnight)
)

# Puzzle 1
# A says "We are both knaves."
# B says nothing.
knowledge1 = And(
    # either knight or knave, not both
    Or(And(AKnight, Not(AKnave)), And(AKnave, Not(AKnight))),
    Or(And(BKnight, Not(BKnave)), And(BKnave, Not(BKnight))),
    # if what a saying true then knight
    Biconditional(And(AKnave, BKnave), AKnight),
    # else they lied and what they said is false
    Biconditional(Not(And(AKnave, BKnave)), AKnave)
)

# Puzzle 2
# A says "We are the same kind."
# B says "We are of different kinds."
knowledge2 = And(
    # either knight or knave, not both
    Or(And(AKnight, Not(AKnave)), And(AKnave, Not(AKnight))),
    Or(And(BKnight, Not(BKnave)), And(BKnave, Not(BKnight))),
    # what a is saying is right else lying
    Biconditional(Or(And(AKnight, BKnight), And(AKnave, BKnave)), AKnight),
    # what b is saying is right else lying
    Biconditional(Or(And(AKnight, BKnave), And(AKnave, BKnight)), BKnight)
)

# Puzzle 3
# A says either "I am a knight." or "I am a knave.", but you don't know which.
# B says "A said 'I am a knave'."
# B says "C is a knave."
# C says "A is a knight."
knowledge3 = And(
    # either knight or knave, not both or none
    Or(And(AKnight, Not(AKnave)), And(AKnave, Not(AKnight))),
    Or(And(BKnight, Not(BKnave)), And(BKnave, Not(BKnight))),
    Or(And(CKnight, Not(CKnave)), And(CKnave, Not(CKnight))),
    # if what b said is true then what a said its a knave, since its a knave then it must be lying so not a knave
    Biconditional(Biconditional(AKnave, BKnight), Not(AKnave)),
    # what b says is true else he knave and opp true
    Biconditional(AKnave, BKnight),
    Biconditional(Not(AKnave), BKnave),
    Biconditional(CKnave, BKnight),
    Biconditional(Not(CKnave), BKnave),
    # what c says is true else he knave and opp true
    Biconditional(AKnight, CKnight),
    Biconditional(Not(AKnight), CKnave)
)


def main():
    symbols = [AKnight, AKnave, BKnight, BKnave, CKnight, CKnave]
    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()
