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

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

case class Heyawake(m: Int, n: Int, board: Seq[Seq[String]]) extends BoardPuzzle {
  def areaName(cell: Cell) = at(cell).split(":")(0)
  val areaNames = cells.map(areaName).toSet
  val areaSize = {
    for (cell <- cells; if at(cell).contains(":"))
    yield areaName(cell) -> at(cell).split(":")(1).toInt
  }.toMap
  val areaCells =
    areaNames.map(name => name -> cells.filter(cell => areaName(cell) == name).toSet).toMap
  val badBlocks: Seq[Seq[Cell]] = {
    def findBlock(cell: Cell, dij: Cell, name: String, block0: Seq[Cell]): Option[Seq[Cell]] =
      if (! isCell(cell)) None
      else if (areaName(cell) != name) Some((cell +: block0).reverse)
      else findBlock(move(cell, dij), dij, name, cell +: block0)
    for {
      dij <- Seq((0,1), (1,0)); i <- 0 until m; j <- 0 until n
      cell = (i,j); cell1 = move(cell, dij)
      if isCell(cell1) && areaName(cell) != areaName(cell1)
      block <- findBlock(cell1, dij, areaName(cell1), Seq(cell))
    } yield block
  }
  def show(sol: Set[Cell]) {
    for (i <- 0 until m) {
      for (j <- 0 until n)
	if (sol.contains((i,j))) print(" ..")
	else print(" ##")
      println
    }
  }
}

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

  val name = "heyawake.Solver"
  var whiteComponents: Set[Set[Cell]] = _

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

  def define = {
    for (cell <- puzzle.cells)
      int('x(cell), 0, 1)
    for (cell <- puzzle.cells; cell1 <- puzzle.adjCells(cell); if cell < cell1)
      add(('x(cell) === 0) || ('x(cell1) === 0))
    for (area <- puzzle.areaNames)
      if (puzzle.areaSize.contains(area)) {
	val xs = puzzle.areaCells(area).map(cell => 'x(cell))
	add(Add(xs) === puzzle.areaSize(area))
      }
    for (block <- puzzle.badBlocks)
      add(Or(block.map(cell => 'x(cell) =/= 0)))
    if (puzzle.m >= 3 || puzzle.n >= 3) {
      for (cell <- puzzle.cells)
	add(('x(cell) === 0) ==> Or(puzzle.adjCells(cell).map(cell1 => 'x(cell1) === 0)))
    }
  }

  def checkSolution: Boolean = {
    val nodes = puzzle.cells.filter(cell => solution('x(cell)) == 0).toSet
    def nextCells(cell: Cell) =
      puzzle.adjCells(cell).filter(cell1 => solution('x(cell1)) == 0).toSet
    val arcs = nodes.map(cell => cell -> nextCells(cell)).toMap
    whiteComponents = getComponents(nodes, arcs)
    if (verbose >= 2)
      println("Components = " + whiteComponents.size)
    whiteComponents.size == 1
  }
  def addNegation {
    for (whites <- whiteComponents) {
      val blacks = for (cell <- whites; cell1 <- puzzle.adjCells(cell); if solution('x(cell1)) > 0)
		   yield cell1
      add(Or(whites.map(cell => 'x(cell) > 0)) || Or(blacks.map(cell => 'x(cell) === 0)))
    }
  }
  override def findFirstSolution = findIncremental(true, checkSolution, addNegation)
  override def findNextSolution = findIncremental(false, checkSolution, addNegation)

  def showSolution {
    val sol = puzzle.cells.filter(cell => solution('x(cell)) == 0).toSet
    if (quiet == 0) {
      println("Solution = " + sol)
      println("Size = " + sol.size)
      puzzle.show(sol)
    }
  }
}