/*

  Langford's number problem with domain tracing in Picat.

  See http://hakank.org/picat/langford.pi

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

*/

import util.
import cp.
import trace_domains.

main => go.

go =>
  K = 12,
  printf("K: %d\n", K),
  time2(langford(K, Solution, Position)),
  trace_domains1d(Solution,solution,"Solution after solve"),
  trace_domains1d(Position,position,"Position after solve"),

  printf("Solution: %w\n", Solution),
  printf("Position: %w\n", Position),

  nl.

langford(K, Solution, Position) =>

  if not ((K mod 4 == 0; K mod 4 == 3)) then
    println("There is no solution for K unless K mod 4 == 0 or K mod 4 == 3"),
    fail
  end,

  K2 = 2*K,
  Position = new_list(K2),
  Position :: 1..K2,

  reset_trace_domains(solution),
  reset_trace_domains(position),

  trace_domains1d(Position,position,"Position Init"),

  Solution = new_list(K2),
  Solution :: 1..K,

  trace_domains1d(Solution,solution,"Solution Init"),

  % symmetry breaking:
  Solution[1] #< Solution[K2],
  trace_domains1d(Position,position,"Position after 1 #< 2"),
  trace_domains1d(Solution,solution,"Solution after 1 #< 2"),

  % all_different(Position),
  all_distinct(Position),
  trace_domains1d(Position,position,"Position after all_different"),

  foreach(I in 1..K)
    Position[K+I] #= Position[I] + I+1,
    element(Position[I],Solution,I),  
    element(Position[K+I],Solution,I),

    trace_domains1d(Position,position,"Position Loop I"=I),
    trace_domains1d(Solution,solution,"Solution Loop I"=I)
  end,

  trace_domains1d(Position,position,"Position before solve"),
  trace_domains1d(Solution,solution,"Solution before solve"),

  Vars = Solution ++ Position,
  solve([ff,updown], Vars).