***
*** 15-puzzle using the generic branch and bound algorithm
***
*** The basic problem setting is copied from the generic backtracking instance
***

sload ../../games/15puzzle
sload branchBound

mod BB-15PUZZLE is
	protecting 15PUZZLE-BIS .
	protecting EXT-BOOL .

	sort Move MoveList State StateList Score Unit .
	subsort Move < MoveList .
	subsort State < StateList .

	*** Constants representing the moves
	ops left right down up : -> Move [ctor] .

	*** Lists of moves
	op nil : -> MoveList [ctor] .
	op __ : MoveList MoveList -> MoveList [ctor assoc id: nil] .

	op size : MoveList -> Nat .

	eq size((nil).MoveList) = 0 .
	eq size(M ML) = s(size(ML)) .

	*** Search states
	op <_=>_> : MoveList Puzzle -> State [ctor] .

	*** Lists of search states as required by the BB framework
	op none : -> StateList [ctor] .
	op __ : StateList StateList -> StateList [ctor assoc id: none] .

	*** A unit type to instantiate the FixData of the BB framework
	op unit : -> Unit [ctor] .

	*** A score is a pair whose first coordinate is the Manhattan distance
	*** to the solved form, and the second is the number of moves
	op {_,_} : Nat Nat -> Score [ctor] .

	op _<_ : Score Score -> Bool .

	*** Lexicographic order may not be convenient
	***eq {X, Y} < {X', Y'} = X < X' or (X == X' and Y < Y') .
	eq {X, Y} < {X', Y'} = X + Y < X' + Y' .

	*** Calculates the score of a state
	op getScore : State Unit -> Score .

	eq getScore(< ML => P >, unit) = { manhattanDistance(P), size(ML) } .

	op manhattanDistance : Puzzle -> Nat .

	eq manhattanDistance(empty) = 0 .
	eq manhattanDistance([X, Y, b] P) = sd(X, 3) + sd(Y, 3) + manhattanDistance(P) .
	eq manhattanDistance([X, Y, N] P) = sd(X, sd(N, 1) rem 4) + sd(Y, sd(N, 1) quo 4) + manhattanDistance(P) .

	*** Is this state a result? It is if the current puzzle is a solution.
	op result? : State Unit -> Bool .

	eq result?(< ML => P >, unit) = manhattanDistance(P) == 0 .

	*** Generic move rule
	crl [move] : < ML => P > => < ML M => P' > if P => P' [nonexec] .

	*** Generic move that prevents undoing the last movement
	crl [move-undo] : < nil => P > => < M => P' > if P => P' [nonexec] .
	crl [move-undo] : < ML LastM => P > => < ML LastM M => P' > if M =/= opposite(LastM) /\ P => P' [nonexec] .

	op opposite : Move -> Move .

	eq opposite(right) = left .
	eq opposite(left) = right .
	eq opposite(up) = down .
	eq opposite(down) = up .

	*** Variables
	vars X Y X' Y' N : Nat .
	vars P P'        : Puzzle .
	var  T           : Tile .
	var  M LastM     : Move .
	var  ML          : MoveList .
endm

smod BB-15PUZZLE-STRAT is
	protecting BB-15PUZZLE .

	strat expand : Unit @ State .
	strat expand : Unit Score @ State .

	sd expand(unit) := move-undo[M <- right]{right}
	                 | move-undo[M <- left]{left}
 	                 | move-undo[M <- down]{down}
                         | move-undo[M <- up]{up} .

	sd expand(unit, B) := expand(unit) ;
	                      match S s.t. getScore(S, unit) < B .

	*** Variables
	var M : Move .
	var B : Score .
	var S : State .
endsm

view 15Puzzle from BB-PROBLEM to BB-15PUZZLE-STRAT is
	sort Value to Score .
	sort PartialResult to State .
	sort PRList to StateList .
	sort FixData to Unit .

	op getBound to getScore .
	op getValue to getScore .
endv

mod EXAMPLES-BIS is
	protecting 15PUZZLE-BIS .

	ops solved puzzle1 puzzle2 wikipedia : -> Puzzle .

	eq solved =	[0,0,1]  [1,0,2]  [2,0,3]  [3,0,4]
			[0,1,5]  [1,1,6]  [2,1,7]  [3,1,8]
			[0,2,9]  [1,2,10] [2,2,11] [3,2,12]
			[0,3,13] [1,3,14] [2,3,15] [3,3,b] .

	eq puzzle1 =	[0,0,b]  [1,0,6]  [2,0,2]  [3,0,4]
			[0,1,1]  [1,1,5]  [2,1,3]  [3,1,8]
			[0,2,9]  [1,2,10] [2,2,7]  [3,2,11]
			[0,3,13] [1,3,14] [2,3,15] [3,3,12] .

	eq puzzle2 =	[0,0,5]  [1,0,1]  [2,0,4]  [3,0,8]
			[0,1,2]  [1,1,14] [2,1,15] [3,1,3]
			[0,2,9]  [1,2,7]  [2,2,6]  [3,2,11]
			[0,3,13] [1,3,10] [2,3,b]  [3,3,12] .

	eq wikipedia =	[0,0,15] [1,0,2]  [2,0,1]  [3,0,12]
			[0,1,8]  [1,1,5]  [2,1,6]  [3,1,11]
			[0,2,4]  [1,2,9]  [2,2,10] [3,2,7]
			[0,3,3]  [1,3,14] [2,3,13] [3,3,b] .
endm

smod MAIN is
	protecting EXAMPLES-BIS .
	protecting BB-STRAT{15Puzzle} .
endsm

eof

srew initial(< nil => puzzle2 >, unit) using solve .

*** Solution 1
*** rewrites: 82966747 in 1305093ms cpu (1312075ms real) (63571 rewrites/second)
*** result BBState: solution(< left left down left up right up up left down right right down right up left down left up right down right up left down down right => [0,0,1] [0,1,5] [0,2,9] [0,3,13] [1,0,2] [1,1,6] [1,2,10] [1,3,14] [2,0,3] [2,1,7] [2,2,11] [2,3,15] [3,0,4] [3,1,8] [3,2,12] [3,3,h] >, {0,27})

*** Solution 1 (in another execution, after some implementation details changed)
*** rewrites: 82966704 in 688803ms cpu (689828ms real) (120450 rewrites/second)
*** result BBState: solution(< up up right up left down left left up right down down right down left up right up left down right down left up right right down => [0,0,1] [0,1,5] [0,2,9] [0,3,13] [1,0,2] [1,1,6] [1,2,10] [1,3,14] [2,0,3] [2,1,7] [2,2,11] [2,3,15] [3,0,4] [3,1,8] [3,2,12] [3,3,h] >, {0,27})

dsrew [1] initial(< nil => puzzle1 >, unit) using solve .

*** Solution 1
*** rewrites: 7116 in 26ms cpu (24ms real) (267649 rewrites/second)
*** result BBState: solution(< down right up right down down right down => [0,0,1] [0,1,5] [0,2,9] [0,3,13] [1,0,2] [1,1,6] [1,2,10] [1,3,14] [2,0,3] [2,1,7] [2,2,11] [2,3,15] [3,0,4] [3,1,8] [3,2,12] [3,3,h] >, {0,8})