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(
	Or(AKnave, AKnight),
	And(AKnave, Not(AKnight)),
	Implication(And(AKnight, AKnave), AKnave) 
)

# Puzzle 1
# A says "We are both knaves."
# B says nothing.
knowledge1 = And(
	Or(AKnave, AKnight),
	Or(BKnave, BKnight),
	Or(And(AKnave, BKnight), And(AKnave, BKnave)),
	Implication(And(AKnave, BKnave), And(AKnave, BKnight))
)

# Puzzle 2
# A says "We are the same kind."
# B says "We are of different kinds."
knowledge2 = And(
	Or(And(AKnave, BKnave), And(AKnight, BKnight), And(AKnave, BKnight)),
	Biconditional(AKnave, Not(AKnight)),
	Biconditional(BKnave, Not(BKnight)),
	Implication(AKnave, Not(And(AKnave, BKnave))),
	Implication(BKnight, And(AKnave, 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(
	Or(AKnave, AKnight),
	Or(BKnave, BKnight),
	Or(CKnave, CKnight),
	Biconditional(AKnave, Not(AKnight)),
	Biconditional(BKnave, Not(BKnight)),
	Biconditional(CKnave, Not(CKnight)),
	
	Implication(AKnave, Not(AKnave)),
	Implication(BKnight, And(AKnave, CKnave)),
	Implication(BKnave, And(AKnight, CKnight)),
	Implication(CKnight, And(AKnight, BKnave))
)


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