/*
 * Masyu Solver in Copris
 * by Naoyuki Tamura
 * http://bach.istc.kobe-u.ac.jp/copris/puzzles/masyu/
 */
package masyu

import jp.kobe_u.copris._
import jp.kobe_u.copris.dsl._
import puzzle._

case class Masyu(m: Int, n: Int, board: Seq[Seq[String]]) extends BoardPuzzle {
  def isWhite(cell: Cell) = at(cell) == "w"
  def isBlack(cell: Cell) = at(cell) == "b"
  def isBlank(cell: Cell) = at(cell) == "-"
  def adj2(cell: Cell) = {
    val (i,j) = cell
    for ((di,dj) <- dijs; if isCell((i+di,j+dj)) && isCell((i-di,j-dj)))
    yield ((i+di,j+dj), (i-di,j-dj))
  }
  def show(sol: Seq[Cell]) {
    val arcs = sol.sliding(2).map(e => (e(0),e(1))).toSet
    def connected(cell1: Cell, cell2: Cell) =
      arcs.contains((cell1,cell2)) || arcs.contains((cell2,cell1))
    for (i <- 0 until m) {
      print(" .")
      for (j <- 0 until n) {
	val cell = (i,j); val cell1 = (i-1,j)
	if (isCell(cell1) && connected(cell, cell1)) print(" | .")
	else print("   .")
      }
      println
      if (i < m) {
	for (j <- 0 until n) {
	val cell = (i,j); val cell1 = (i,j-1)
	  if (isCell(cell1) && connected(cell, cell1)) print("---")
	  else print("   ")
	  if (isBlank(cell)) print("+")
	  else print(at(cell))
	}
	println("  ")
      }
    }
    println(" ." + "   ." * n)
  }
}

object Solver extends BoardPuzzleSolver[Masyu] {
  import scala.math.Ordering.Implicits._

  val name = "masyu.Solver"
  var cycles: Set[Seq[Cell]] = _

  def puzzleFactory(m: Int, n: Int, board: Seq[Seq[String]]) =
    Masyu(m, n, board)

  def define = {
    for (cell <- puzzle.cells; cell1 <- puzzle.adjCells(cell))
      int('e(cell,cell1), 0, 1)
    for (cell <- puzzle.cells; cell1 <- puzzle.adjCells(cell); if cell < cell1)
      add('e(cell,cell1) + 'e(cell1,cell) <= 1)
    for (cell <- puzzle.cells) {
      val in = puzzle.adjCells(cell).map(cell1 => 'e(cell1,cell))
      val ot = puzzle.adjCells(cell).map(cell1 => 'e(cell,cell1))
      int('io(cell), 0, 1)
      add('io(cell) === Add(in))
      add('io(cell) === Add(ot))
      if (puzzle.isWhite(cell) || puzzle.isBlack(cell))
	add('io(cell) === 1)
    }
    // Straight line
    for (cell <- puzzle.cells) {
      int('s(cell), 0, 1)
      val s = for ((cell1,cell2) <- puzzle.adj2(cell))
	      yield ('e(cell1,cell) === 1) && ('e(cell,cell2) === 1)
      add(('s(cell) === 1) <==> Or(s))
    }
    for (cell <- puzzle.cells) {
      if (puzzle.isWhite(cell)) {
	add('s(cell) === 1)
	for ((cell1,cell2) <- puzzle.adj2(cell))
	  add((('e(cell1,cell) === 1) || ('e(cell,cell1) === 1)) ==>
  	      (('s(cell1) === 0) || ('s(cell2) === 0)))
      } else if (puzzle.isBlack(cell)) {
	add('s(cell) === 0)
	for (cell1 <- puzzle.adjCells(cell))
	  add((('e(cell1,cell) === 1) || ('e(cell,cell1) === 1)) ==>
	      ('s(cell1) === 1))
      }
    }
  }

  def checkSolution: Boolean = {
    val nodes = puzzle.cells.filter(cell => solution('io(cell)) > 0).toSet
    def nextCells(cell: Cell) =
      puzzle.adjCells(cell).filter(cell1 => solution('e(cell,cell1)) > 0).toSet
    val arcs = nodes.map(cell => cell -> nextCells(cell)).toMap
    cycles = getCycles(nodes, arcs)
    cycles = cycles.filter(cycle => cycle.exists(cell => ! puzzle.isBlank(cell)))
    if (verbose >= 2)
      println("Cycles = " + cycles.size)
    cycles.size == 1
  }
  def addNegation {
    for (cycle <- cycles) {
      add(Or(cycle.sliding(2).map(e => 'e(e(0),e(1)) === 0).toSeq))
      add(Or(cycle.reverse.sliding(2).map(e => 'e(e(0),e(1)) === 0).toSeq))
    }
  }
  override def findFirstSolution = findIncremental(true, checkSolution, addNegation)
  override def findNextSolution = findIncremental(false, checkSolution, addNegation)

  def showSolution {
    // Cycle
    require(cycles.size == 1)
    val sol = cycles.head
    if (quiet == 0) {
      println("Solution = " + sol)
      println("Size = " + sol.size)
      puzzle.show(sol)
    }
  }
}