sbv-8.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright(c) Levent Erkok
Safe HaskellNone




You are standing in front of three rooms and must choose one. In one room is a Lady (whom you could and wish to marry), in the other two rooms are tigers (that if you choose either of these rooms, the tiger invites you to breakfast – the problem is that you are the main course). Your job is to choose the room with the Lady. The signs on the doors are:

  • A Tiger is in this room
  • A Lady is in this room
  • A Tiger is in room two

At most only 1 statement is true. Where’s the Lady?



ladyAndTigers :: IO AllSatResult Source #

Prints the only solution:

>>> ladyAndTigers
Solution #1:
  sign1  = False :: Bool
  sign2  = False :: Bool
  sign3  =  True :: Bool
  tiger1 = False :: Bool
  tiger2 =  True :: Bool
  tiger3 =  True :: Bool
This is the only solution.

That is, the lady is in room 1, and only the third room's sign is true.