#!/usr/bin/perl
# Talos Principle puzzle solver
# (c) 2015 Norbert Preining
# Licensed under GPLv3 or any higher version
# http://www.preining.info/blog/2015/06/talos-principle-puzzles-sat-solvers/

use strict;
$^W = 1;

# riddle1
#create_smt2_def(5,8,'sl','sl','sr','a','a','b','b','cl','cl','q');
# riddle2
#create_smt2_def(4,10,'sr','a','a','a','a','q','q','b','cl','cl');
#create_smt2_def(4,7,'cl','cr','sl','sl','a','a','b');
create_smt2_def(8,6,'a','a','b','cl','cl','cr','cr','cr','q','q','sl','sl');
#create_smt2_def(6,6,'b','q','q','sl','sl','cl','cl','cr','cr');

sub create_smt2_def {
  my ($xx, $yy, @pieces) = @_ ;
  my $nn = $#pieces + 1;

  # print header
  print "(set-option :produce-models true)\n";
  print "(set-logic QF_UF)\n";

  # start with declaring variables
  for my $i (1..$xx) {
    for my $j (1..$yy) {
      for my $n (1..$nn) {
        print "(declare-fun x_${i}_${j}_$n () Bool)\n"
      }
    }
  }
  # at least one
  for my $i (1..$xx) {
    for my $j (1..$yy) {
      print "(assert (or";
      for my $n (1..$nn) {
        print " x_${i}_${j}_${n}";
      }
      print "))\n";
    }
  }
  # at most one
  for my $i (1..$xx) {
    for my $j (1..$yy) {
      print "(assert (and\n";
      for my $n (1..$nn) {
        for my $m ($n..$nn) {
          next if ($n == $m) ;
          print "  (not (and x_${i}_${j}_${n} x_${i}_${j}_${m}))\n";
	}
      }
      print "))\n";
    }
  }

  # every piece is used at least once
  for my $n (1..$nn) {
    print "(assert (or";
    for my $i (1..$xx) {
      for my $j (1..$yy) {
        print " x_${i}_${j}_$n";
      }
    }
    print "))\n";
  }
        
  # for each piece, call the defining assertions
  for my $n (1..$nn) {
    my $p = $pieces[$n-1];
    print "(assert (or\n";
    for my $i (1..$xx) {
      for my $j (1..$yy) {
        if ($p eq 'q') { 
          type_square($xx,$yy,$i,$j,$n); 
        } elsif ($p eq 'cr') { 
          type_club_right($xx,$yy,$i,$j,$n);
        } elsif ($p eq 'cl') { 
          type_club_left($xx,$yy,$i,$j,$n);
        } elsif ($p eq 'sr') { 
          type_step_right($xx,$yy,$i,$j,$n); 
        } elsif ($p eq 'sl') { 
          type_step_left($xx,$yy,$i,$j,$n); 
        } elsif ($p eq 'b') {
          type_stick($xx,$yy,$i,$j,$n);
        } elsif ($p eq 'a') {
          type_potest($xx,$yy,$i,$j,$n);
        } else {
          die "Unknown type $p";
        }
      }
    }
    print "))\n";
  }
  print "(check-sat)\n(get-model)\n";
}

sub same_ij {
  my (@pairs) = @_;
  my %f;
  while (@pairs) {
    my $i = shift @pairs;
    my $j = shift @pairs;
    if (defined($f{$i}{$j})) {
      return 1;
    } else {
      $f{$i}{$j} = 1;
    }
  }
  return 0;
}

sub check {
  my ($xx,$yy, @pairs) = @_;
  while (@pairs) {
    my $i = shift @pairs;
    my $j = shift @pairs;
    if ($i < 1 || $i > $xx || $j < 1 || $j > $yy) {
      return 0;
    }
  }
  return 1;
}

sub check_and_shipout {
  my ($xx,$yy, $n, @pairs) = @_;
  if (check($xx,$yy, @pairs)) {
    print "  (and";
    while (@pairs) {
      my $i = shift @pairs;
      my $j = shift @pairs;
      print " x_${i}_${j}_$n";
    }
    print ")\n";
  }
}

sub rotate90 {
  my ($i, $j, @pairs) = @_ ;
  my @ret;
  while (@pairs) {
    my $ii = shift @pairs;
    my $jj = shift @pairs;
    my $ni = $i - ($jj - $j);
    my $nj = $j + ($ii - $i);
    push @ret, $ni, $nj;
  }
  return @ret;
}

sub do_rotate_shipout {
  my ($xx,$yy, $i, $j, $n, @pairs) = @_ ;
  for my $g (0..3) {
    @pairs = rotate90($i, $j, @pairs);
    check_and_shipout($xx,$yy, $n, $i, $j, @pairs);
  }
}

# type square
# Or
# lu
sub type_square {
  my ($xx,$yy, $i,$j,$n) = @_;
  my ($il, $jl, $ir, $jr, $iu, $ju);
  $il = $i; $iu = $ir = $i + 1;
  $jl = $ju = $j - 1; $jr = $j;
  do_rotate_shipout($xx,$yy, $i, $j, $n, $il, $jl, $ir, $jr, $iu, $ju);
}

# type club right
#   u
#   Olr
sub type_club_right {
  my ($xx,$yy, $i,$j,$n) = @_;
  my ($il, $jl, $ir, $jr, $iu, $ju);
  $il = $i + 1; $iu = $i, $ir = $i + 2;
  $jl = $jr = $j; $ju = $j + 1;
  do_rotate_shipout($xx,$yy, $i, $j, $n, $il, $jl, $ir, $jr, $iu, $ju);
}

#
# type club left
#   Olr
#   u
sub type_club_left {
  my ($xx,$yy, $i,$j,$n) = @_;
  my ($il, $jl, $ir, $jr, $iu, $ju);
  $il = $i + 1; $iu = $i, $ir = $i + 2;
  $jl = $jr = $j; $ju = $j - 1;
  do_rotate_shipout($xx,$yy, $i, $j, $n, $il, $jl, $ir, $jr, $iu, $ju);
}

# type step left
# lu
#  Or
sub type_step_left {
  my ($xx,$yy, $i,$j,$n) = @_;
  my ($il, $jl, $ir, $jr, $iu, $ju);
  $il = $i - 1; $iu = $i, $ir = $i + 1;
  $jl = $ju = $j + 1; $jr = $j;
  do_rotate_shipout($xx,$yy, $i, $j, $n, $il, $jl, $ir, $jr, $iu, $ju);
}

#
# type step right
#  ur
# lO
sub type_step_right {
  my ($xx,$yy, $i,$j,$n) = @_;
  my ($il, $jl, $ir, $jr, $iu, $ju);
  $il = $i - 1; $iu = $i, $ir = $i + 1;
  $jl = $j; $ju = $jr = $j + 1;
  do_rotate_shipout($xx,$yy, $i, $j, $n, $il, $jl, $ir, $jr, $iu, $ju);
}


# type long stick OXXX
# anchor point left most
sub type_stick {
  my ($xx,$yy, $i, $j, $n) = @_;
  my ($ii, $jj, $iii, $jjj, $iiii, $jjjj);
  $jj = $jjj = $jjjj = $j;
  $ii = $i + 1; $iii = $i + 2; $iiii = $i + 3;
  do_rotate_shipout($xx,$yy, $i, $j, $n, $ii, $jj, $iii, $jjj, $iiii, $jjjj);
}


#
# type winner potest
#      u
#     lOr
# anchor point center
sub type_potest {
  my ($xx,$yy,$i,$j,$n) = @_;
  my ($il, $jl, $ir, $jr, $iu, $ju);
  $il = $i - 1; $ir = $i + 1; $iu = $i;
  $jl = $jr = $j; $ju = $j + 1;
  do_rotate_shipout($xx,$yy, $i, $j, $n, $il, $jl, $ir, $jr, $iu, $ju);
}