3 import StdList, StdInt, StdBool, StdChar, StdMisc, StdClass, StdString, StdFile, StdArray, StdTuple, Data.Maybe, Data.Map, Control.Monad, Data.Tuple, Data.Void
6 inpath :== "screen.1001"
7 outpath :== "solver.smv"
9 checkX :: [[SokobanTile]] Int -> Int
10 checkX p x = if (x > (length p - 1)) (-1) x
12 checkY :: [[SokobanTile]] Int Int -> Int
14 | ((x < 0) || (x > (length p - 1))) = -1
15 | otherwise = if (y > (length (p !! x) - 1)) (-1) y
17 genField :: [[SokobanTile]] Int Int -> String
18 genField p x y = " init(x" +++ toString x +++ "_" +++ toString y +++ ") := " +++ fromTile ((p !! x) !! y) +++ ";\n"
20 genVars :: Int Int -> String
21 genVars x y = " x" +++ toString x +++ "_" +++ toString y +++ " : {Wall, Free, Box, BoxOnTarget, Target, Agent, AgentOnTarget};\n"
23 genCoord :: [[SokobanTile]] Int Int -> [String]
24 genCoord p x y = [" next(x" +++ toString x +++ "_" +++ toString y +++ ") := case\n",
25 " x" +++ toString x +++ "_" +++ toString y +++ " = Wall: Wall;\n",
26 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent | x"
27 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = AgentOnTarget) & move = Left: Agent;\n",
28 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent | x"
29 +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = AgentOnTarget) & move = Up: Agent;\n",
30 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x"
31 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & move = Right : Agent;\n",
32 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent | x"
33 +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = AgentOnTarget) & move = Down : Agent;\n",
35 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Box | x"
36 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Agent | x"
37 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = AgentOnTarget) & move = Left: Box;\n",
38 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Box | x"
39 +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Agent | x"
40 +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = AgentOnTarget) & move = Up: Box;\n",
41 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box | x"
42 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Agent | x"
43 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = AgentOnTarget) & move = Right : Box;\n",
44 " x" +++ toString x +++ "_" +++ toString y +++ " = Free & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box | x"
45 +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Agent | x"
46 +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = AgentOnTarget) & move = Down : Box;\n",
48 " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Target) & move = Right: Free;\n",
49 " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Target) & move = Down: Free;\n",
50 " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left : Free;\n",
51 " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ "= Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up : Free;\n",
53 " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Box | x"
54 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = BoxOnTarget) & (x"
55 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Target) & move = Right: Free;\n",
56 " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Box | x"
57 +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = BoxOnTarget) & (x"
58 +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Free | x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Target) & move = Down: Free;\n",
59 " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box | x"
60 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = BoxOnTarget) & (x"
61 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Target) & move = Left: Free;\n",
62 " x" +++ toString x +++ "_" +++ toString y +++ " = Agent & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box | x"
63 +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = BoxOnTarget) & (x"
64 +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Free | x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Target) & move = Up: Free;\n",
66 " x" +++ toString x +++ "_" +++ toString y +++ " = Box & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent | x"
67 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = AgentOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left: Agent;\n",
68 " x" +++ toString x +++ "_" +++ toString y +++ " = Box & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent | x"
69 +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = AgentOnTarget) & (x" +++ toString (x-1) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up: Agent;\n",
70 " x" +++ toString x +++ "_" +++ toString y +++ " = Box & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x"
71 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Target) & move = Right : Agent;\n",
72 " x" +++ toString x +++ "_" +++ toString y +++ " = Box & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent | x"
73 +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = AgentOnTarget) & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p x y) +++ " = Target) & move = Down : Agent;\n",
75 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent | x"
76 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = AgentOnTarget) & move = Left: AgentOnTarget;\n",
77 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent | x"
78 +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = AgentOnTarget) & move = Up: AgentOnTarget;\n",
79 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x"
80 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & move = Right : AgentOnTarget;\n",
81 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent | x"
82 +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = AgentOnTarget) & move = Down : AgentOnTarget;\n",
84 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Box | x"
85 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = Agent | x"
86 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+2)) +++ " = AgentOnTarget) & move = Left: BoxOnTarget;\n",
87 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Box | x"
88 +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = Agent | x"
89 +++ toString (checkX p (x+2)) +++ "_" +++ toString (checkY p (x+2) y) +++ " = AgentOnTarget) & move = Up: BoxOnTarget;\n",
90 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Box | x"
91 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = BoxOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = Agent | x"
92 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-2)) +++ " = AgentOnTarget) & move = Right : BoxOnTarget;\n",
93 " x" +++ toString x +++ "_" +++ toString y +++ " = Target & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Box | x"
94 +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = BoxOnTarget) & (x" +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = Agent | x"
95 +++ toString (checkX p (x-2)) +++ "_" +++ toString (checkY p (x-2) y) +++ " = AgentOnTarget) & move = Down : BoxOnTarget;\n",
97 " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Target) & move = Right: Target;\n",
98 " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Target) & move = Down: Target;\n",
99 " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left : Target;\n",
100 " x" +++ toString x +++ "_" +++ toString y +++ " = AgentOnTarget & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up : Target;\n",
102 " x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Agent | x"
103 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = AgentOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Free | x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Target) & move = Left: AgentOnTarget;\n",
104 " x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Agent | x"
105 +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = AgentOnTarget) & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Free | x" +++ toString (checkX p (x-1)) +++ "_"
106 +++ toString (checkY p (x-1) y) +++ " = Target) & move = Up: AgentOnTarget;\n",
107 " x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = Agent | x"
108 +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y-1)) +++ " = AgentOnTarget) & (x" +++ toString (checkX p x) +++ "_" +++ toString (checkY p x (y+1)) +++ " = Free | x" +++ toString x +++ "_" +++ toString (checkY p x (y+1)) +++ " = Target) & move = Right : AgentOnTarget;\n",
109 " x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget & (x" +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = Agent | x"
110 +++ toString (checkX p (x-1)) +++ "_" +++ toString (checkY p (x-1) y) +++ " = AgentOnTarget) & (x" +++ toString (checkX p (x+1)) +++ "_" +++ toString (checkY p (x+1) y) +++ " = Free | x" +++ toString (checkX p (x+1)) +++ "_"
111 +++ toString (checkY p (x+1) y) +++ " = Target) & move = Down : AgentOnTarget;\n",
113 " TRUE : x" +++ toString x +++ "_" +++ toString y +++ ";\n",
117 instance == SokobanTile
119 (==) Wall Wall = True
120 (==) Free Free = True
122 (==) Agent Agent = True
123 (==) Target Target = True
124 (==) TargetBox TargetBox = True
125 (==) TargetAgent TargetAgent = True
128 fromTile :: SokobanTile -> String
129 fromTile Wall = "Wall"
130 fromTile Free = "Free"
132 fromTile Target = "Target"
133 fromTile Agent = "Agent"
134 fromTile TargetAgent = "AgentOnTarget"
135 fromTile TargetBox = "BoxOnTarget"
137 genCond :: [[SokobanTile]] Int Int -> String
139 | x < 0 || y < 0 || x > (length p) - 1 = ""
141 | y > (length (p !! x) - 1) = ""
142 | otherwise = if ((p !! x) !! y == Target) ("x" +++ toString x +++ "_" +++ toString y +++ " = BoxOnTarget") ""
144 addLogic :: [String] -> [String]
147 addLogic [x:xs] = [x +++ " & ": addLogic xs]
149 genAll :: SokobanPuzzle -> [String]
150 genAll puzzle = let (Sokoban p) = puzzle in
155 ++ [genVars x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
156 ++ [" move : {Up, Down, Left, Right};\n"]
159 " init(move) := {Up, Down, Left, Right};\n"
161 ++ [genField p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
162 ++ flatten [filter (\x -> not (contains '-' x)) (genCoord p x y) \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]]
163 ++ [" next(move) := {Up, Down, Left, Right};\n"]
165 ++ addLogic (filter (\x -> x <> "" ) [genCond p x y \\ x <- [0..(length p - 1)], y <- [0..(length (p !! x) - 1)]])
168 contains :: Char String -> Bool
169 contains char str = not (isEmpty [c\\c<-:str | char == c])
171 readLines :: File -> [String]
174 # (line, file) = sfreadline file
175 | otherwise = [line: readLines file]
177 writeLines :: [String] *File -> *File
178 writeLines [] file = file
179 writeLines [l:ls] file = writeLines ls (file <<< l)
181 openInpFile :: *World String -> (File, *World)
182 openInpFile world path
183 # (ok, file, world) = sfopen path 0 world
184 | not ok = abort "Error reading the file."
187 openOutFile :: *World String -> (*File, *World)
188 openOutFile world path
189 # (ok, file, world) = fopen path 1 world
190 | not ok = abort "Can not write to a file."
193 closeFile :: *World *File -> (Bool, *World)
195 # world = fclose file world
198 Start :: *World -> *World
200 # (p, w) = parse inpath w
202 # (f, w) = openOutFile w outpath
204 # (ok, w) = closeFile w f