package puzzle

import jp.kobe_u.copris._
import jp.kobe_u.copris.dsl._
import scala.io.Source

abstract class AbstractPuzzle {
  type Cell = (Int,Int)
  type Grid = (Int,Int)
}

abstract class BoardPuzzle extends AbstractPuzzle {
  val m: Int
  val n: Int
  val board: Seq[Seq[String]]
  require(board.size == m && m >= 2)
  require(board.forall(_.size == n) && n >= 2)
  val cells = for (i <- 0 until m; j <- 0 until n) yield (i,j)
  def isCell(cell: Cell) = 0 <= cell._1 && cell._1 < m && 0 <= cell._2 && cell._2 < n
  def at(cell: Cell) = board(cell._1)(cell._2)
  def isNumber(cell: Cell) = at(cell).matches("\\d+")
  def num(cell: Cell) = at(cell).toInt
  val numberCells = for (cell <- cells; if isNumber(cell)) yield cell
  def adjCells(cell: Cell, filter: (Cell => Boolean) = {case _ => true}) = {
    val (i,j) = cell
    for (cell1 <- Seq((i-1,j),(i+1,j),(i,j-1),(i,j+1)); if isCell(cell1) && filter(cell1))
    yield cell1
  }
  val dijs = Seq((-1,0), (1,0), (0,-1), (0,1))
  def move(cell: Cell, dij: Cell) = (cell._1+dij._1,cell._2+dij._2)
  val grids = for (i <- 0 to m; j <- 0 to n) yield (i,j)
  def isGrid(cell: Cell) = 0 <= cell._1 && cell._1 <= m && 0 <= cell._2 && cell._2 <= n
  def adjGrids(grid: Grid, filter: (Grid => Boolean) = {case _ => true}) = {
    val (i,j) = grid
    for (grid1 <- Seq((i-1,j),(i+1,j),(i,j-1),(i,j+1)); if isGrid(grid1) && filter(grid1))
    yield grid1
  }
}

trait AbstractPuzzleSolver[PUZZLE <: AbstractPuzzle] {
  val name: String
  var help = false
  var quiet = 0
  var verbose = 0
  var dumpFile: String = _
  var options: Set[String] = Set.empty

  var puzzle: PUZZLE = _
  def puzzleFactory(m: Int, n: Int, board: Seq[Seq[String]]): PUZZLE

  def parse(source: Source): PUZZLE
  def define: Unit
  def findFirstSolution: Boolean = find
  def findNextSolution: Boolean = findNext
  def findOptSolution: Boolean = findOpt
  def showSolution: Unit

  def solve {
    var count = 0
    def _showSolution {
      count += 1
      println("BEGIN_solution = " + count)
      showSolution
      println("END_solution = " + count)
    }

    define
    if (dumpFile != null)
      dump(dumpFile)
    if (options.contains("opt")) {
      if (findOptSolution) {
	_showSolution
	println("NumOfOptSolutions >= 1")
      } else {
	println("NumOfOptSolutions = 0")
      }
    } else {
      if (findFirstSolution) {
	_showSolution
	if (options.contains("all")) {
	  while (findNextSolution) {
	    _showSolution
	  }
	  println("NumOfSolutions = " + count)
	} else if (options.contains("multi")) {
	  if (findNextSolution) {
	    if (verbose >= 2)
	      _showSolution
	    println("NumOfSolutions >= 2")
	  } else {
	    println("NumOfSolutions = 1")
	  }
	} else {
	  println("NumOfSolutions >= 1")
	}
      } else {
	println("NumOfSolutions = 0")
      }
    }
  }

  def main(args: Array[String]) = {
    var fileName = ""
    var solverName = ""
    def parseOptions(args: List[String]): List[String] = args match {
      case "-o" :: opt :: rest =>
	{ options = opt.split(",").toSet; parseOptions(rest) }
      case "-s1" :: solver :: rest => {
	solverName = solver
	val satSolver = new sugar.SatSolver1(solver)
	use(new sugar.Solver(csp, satSolver))
	parseOptions(rest)
      }
      case "-s2" :: solver :: rest => {
	solverName = solver
	val satSolver = new sugar.SatSolver2(solver)
	use(new sugar.Solver(csp, satSolver))
	parseOptions(rest)
      }
      case "-smt" :: solver :: rest => {
	solverName = solver
	val smtSolver = new smt.SmtSolver(solver)
	use(new smt.Solver(csp, smtSolver))
	parseOptions(rest)
      }
      case "-q" :: rest =>
	{ quiet += 1; parseOptions(rest) }
      case "-v" :: rest =>
	{ verbose += 1; parseOptions(rest) }
      case "-dump" :: file :: rest =>
	{ dumpFile = file; parseOptions(rest) }
      case "-h" :: rest =>
	{ help = true; parseOptions(rest) }
      case _ =>
	args
    }
    parseOptions(args.toList) match {
      case Nil if ! help => {
	fileName = "-"
	puzzle = parse(Source.stdin)
      }
      case file :: Nil if ! help => {
	fileName = file
	puzzle = parse(Source.fromFile(file))
      }
      case _ => {
        println("Usage: scala " + name + " [options] [inputFile]")
	println("\t-o options  : Set options ('multi', 'opt', etc.)")
	println("\t-v          : Increase verbosity level")
	println("\t-q          : Increase quiet level")
	println("\t-s1 solver  : Use SAT solver with one argument (clasp, etc.)")
	println("\t-s2 solver  : Use SAT solver with two arguments (minisat, etc.)")
	println("\t-smt solver : Use SMT solver (z3, etc.)")
	println("\t-dump file  : Output Sugar CSP to the specified file")
	println("\t-h          : Show this help message")
	System.exit(1)
      }
    }
    if (verbose >= 1) {
      println("File = " + fileName)
      println("Solver = " + solverName)
      println("Options = " + options.mkString(","))
    }
    solve
    if (verbose >= 2) {
      println("Info  = " + info)
      println("Stats = " + stats)
    }
  }
}

trait BoardPuzzleSolver[PUZZLE <: BoardPuzzle] extends AbstractPuzzleSolver[PUZZLE] {
  type Cell = (Int,Int)
  type Grid = (Int,Int)
  type Node = (Int,Int)

  // override var puzzle: PUZZLE = _
  // override def puzzleFactory(m: Int, n: Int, board: Seq[Seq[String]]): PUZZLE
  def parse(source: Source) = {
    val lines = source.getLines.map(_.trim).filter(! _.startsWith(";"))
    val m = lines.next.toInt
    val n = lines.next.toInt
    val board = for (i <- 0 until m; s = lines.next)
		yield s.split("\\s+").toSeq
    source.close
    puzzleFactory(m, n, board)
  }

  def getComponents(nodes: Set[Node], arcs: Map[Node,Set[Node]]): Set[Set[Node]] = {
    def getComponent(open: Set[Node], closed: Set[Node]): Set[Node] =
      if (open.isEmpty) closed
      else {
	val node = open.head
	val newNodes = for {
	  node1 <- arcs.getOrElse(node, Set.empty)
	  if ! open.contains(node1) && ! closed.contains(node1)
	} yield node1
	getComponent(open.tail ++ newNodes, closed + node)
      }
    var components: Set[Set[Node]] = Set.empty
    var currentNodes = nodes
    while (! currentNodes.isEmpty) {
      val component = getComponent(Set(currentNodes.head), Set.empty)
      components += component
      currentNodes --= component
    }
    components
  }
  def getCycles(nodes: Set[Node], arcs: Map[Node,Set[Node]]): Set[Seq[Node]] = {
    def toCycle(node: Node, component: Set[Node]): Seq[Node] =
      if (component.isEmpty) Seq(node)
      else {
	val node1 = arcs(node).find(node1 => component.contains(node1)).get
	node +: toCycle(node1, component - node1)
      }
    for (component <- getComponents(nodes, arcs))
      yield toCycle(component.head, component)
  }
  def findIncremental(first: Boolean, checkSolution: => Boolean, addNegation: => Unit) = {
    def _findNext: Boolean = {
      addNegation
      find
    }
    var found = false
    if (if (first) find else _findNext) {
      do {
	found = checkSolution
      } while (! found && _findNext)
    }
    found
  }

  override def solve {
    if (verbose >= 1) {
      println("Rows = " + puzzle.m)
      println("Cols = " + puzzle.n)
    }
    super.solve
  }
}