/* 

  Mixed couples on Mars and Venus puzzle in Picat.

  From TPTP, PUZ/PUZ007-1.p
  """
  File     : PUZ007-1 : TPTP v8.2.0. Released v1.0.0.
  Domain   : Puzzles
  Problem  : Mixed couples on Mars and Venus
  Version  : Especial.
  English  : Here's the situation: human observers in this exclusive club
             on Ganymede can't distinguish Martians from Venusians, males
             from females, except for the fact that Venusian women and
             Martian men always tell the truth and Venusian men and
             Martian women always lie.
             A says "I'm from Mars" B exclaims "That's not true!" A and
             B are married; are they a mixed couple?

  ...

  ----Conclude that they are NOT a mixed couple.
  ----Denial of the conclusion: either M(A) & V(B) or V(A) & M(B)
  cnf(one_from_mars,negated_conjecture,
    ( from_mars(b)
    | from_mars(a) ) ).

  cnf(one_from_venus,negated_conjecture,
    ( from_venus(a)
    | from_venus(b) ) ).
  
  """

  I assume that "mixed couple" means that one of the couple is from
  Mars and the other is from Venus.

  This model gives two solutions:
  A: gender:Male place:Mars truth:true
  B: gender:Female place:Mars truth:false

  A: gender:Male place:Venus truth:false
  B: gender:Female place:Venus truth:true

  Both indicating that A and B are from the same planet, i.e.
  not a mixed couple.
  
  Interestingly, it does not matter if the marrying constraint
  are active or not.


  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 ?=>
  % Gender
  Male = 1, Female = 2, 
  Gender = [AG,BG],
  Gender = [Male,Female],

  % Place
  Mars = 1, Venus = 2,
  Place = [AP,BP],
  Place :: [Mars,Venus],

  % Truthfulness of the speaker
  Ts = [AT,BT], 
  Ts :: 0..1, 

  % A says "I'm from Mars" 
  AT #<=> AP #= Mars,

  % B exclaims "That's not true!" 
  % BT #<=> AP #!= Mars,
  BT #<=> #~(AP #= Mars),
  % BT #<=> AT #= 0,

  % A and B are married
  % hakank: Let's assume that it's a Male/Female marriage.
  % However, this does not do any difference...
  % (AG #= Male #/\ BG #= Female) #\/ (AG #= Female #/\ BG #= Male),

  % are they a mixed couple?
  

  foreach(I in 1..2)
    % Venusian women and Martian men always tell the truth and  
    (Place[I] #= Venus #/\ Gender[I] #= Female) #=> Ts[I] #= 1,
    (Place[I] #= Mars #/\ Gender[I] #= Male) #=> Ts[I] #= 1,

    % Venusian men and Martian women always lie.
    (Place[I] #= Venus #/\ Gender[I] #= Male) #=> Ts[I] #= 0,
    (Place[I] #= Mars #/\ Gender[I] #= Female) #=> Ts[I] #= 0  
  end,

  Vars = Gender ++ Place ++ Ts,
  solve(Vars),

  GenderMap = new_map([1="Male",2="Female"]),
  PlaceMap = new_map([1="Mars",2="Venus"]),
  
  println(gender=Gender),
  println(place=Place),
  println(ts=Ts),
  printf("A: gender:%w place:%w truth:%w\n",GenderMap.get(AG),PlaceMap.get(AP),cond(AT==1,true,false)),
  printf("B: gender:%w place:%w truth:%w\n",GenderMap.get(BG),PlaceMap.get(BP),cond(BT==1,true,false)),  
  nl,
  fail,

  
  
  nl.
go => true.