/* 

  Minos and aminos: we are both married or both unmarried in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  """
  Puzzle 76. Minos and aminos: we are both married or both unmarried

  According to another version of the story, Oh, Auspicious King, Bahman didn't say
  that they were both married; instead he said, "We are both married or both unmarried".
  If that version is correct, then what can be deduced about Bahman and what can be
  deduced about Perviz? (taken from Smullyan (1996))
  """  

  (See minos_and_aminos_we_are_both_married.pi for the previous puzzle.)

  There are two solutions:

  Bahman:Amino (married: false)  Perviz:Amino (married: true)
  Bahman:Mino (married: false)  Perviz:Mino (married: false)

  In both solutions, Bahman is unmarried. 
  The marital status of Perviz is unknown.


  This program was created by Hakan Kjellerstrand, hakank@gmail.com
  See also my Picat page: http://www.hakank.org/picat/

*/

import cp.

main => go.

go ?=>
  % Amino: Always lies
  % Mino: Always tells the truth
  Amino = 0, Mino = 1,
  [Bahman,Perviz] :: [Amino,Mino],

  [BahmanMarried,PervizMarried] :: 0..1,

  % Thus given any pair of brothers,they are either both Minos or both Aminos.
  Bahman #= Perviz,

  % Bahman: We are both married or both unmarried
  Bahman #<=> (BahmanMarried #= PervizMarried),
  
  % Perviz: I am not married.
  Perviz #<=> PervizMarried #= 0,

  Vars = [bahman=Bahman,perviz=Perviz,bahman_married=BahmanMarried,pervis_married=PervizMarried],
  solve(Vars),
  println(Vars),
  Map = new_map([0="Amino",1="Mino"]),
  printf("Bahman:%w (married: %w)  Perviz:%w (married: %w)\n",
                       Map.get(Bahman),cond(BahmanMarried==1,true,false),
                       Map.get(Perviz),cond(PervizMarried==1,true,false)),
  nl,
  fail,
  
  nl.
go => true.