/* 

  Sex and race on Mars and Venus in Picat.

  From TPTP: PUZ006-1.p
  """
  File     : PUZ006-1 : TPTP v7.0.0. Released v1.0.0.
  Domain   : Puzzles
  Problem  : Determine sex and race 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.
             Ork says "Bog is from Venus."  Bog says "Ork is from Mars."
             Ork says "Bog is male."  Bog says "Ork is female." Who's
             what?  (sex & race).

  ...

  cnf(prove_bog_is_female,negated_conjecture,
    ~ female(bog) ).
  """

  Unique solution: 

  Ork: gender:Male place:Venus truth:false
  Bog: gender:Female place:Mars truth:false

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

*/

% import util.
import cp.

main => go.

go ?=>
  % Gender
  Male = 1, Female = 2, 
  Gender = [OrkG,BogG],
  Gender = [Male,Female],

  % Place
  Mars = 1, Venus = 2,
  Place = [OrkP,BogP],
  Place :: [Mars,Venus],

  % Truthfulness of the speaker
  Ts = [OrkT,BogT], 
  Ts :: 0..1, 

  % Statements

  % % Ork says "Bog is from Venus."  Bog says "Ork is from Mars."
  % OrkT #<=> (BogP #= Venus),
  % BogT #<=> (OrkP #= Mars),

  % % Ork says "Bog is male."  Bog says "Ork is female." 
  % OrkT #<=> (BogG #= Male),
  % BogT #<=> (OrkG #= Female),

  % Simpler:

  % Ork says "Bog is from Venus."  Ork says "Bog is male."  
  OrkT #<=> (BogP #= Venus #/\ BogG #= Male),

  % Bog says "Ork is from Mars." Bog says "Ork is female." 
  BogT #<=> (OrkP #= Mars #/\ OrkG #= Female),



  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("Ork: gender:%w place:%w truth:%w\n",GenderMap.get(OrkG),PlaceMap.get(OrkP),cond(OrkT==1,true,false)),
  printf("Bog: gender:%w place:%w truth:%w\n",GenderMap.get(BogG),PlaceMap.get(BogP),cond(BogT==1,true,false)),  
  nl,
  fail,

  nl.
go => true.