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 } }