This application is similar to the previous one but this time we have to move a horse on a chessboard (3x4) such that the horse passes exactly one time by each position. All the modules and a demo for this program can be found on the horses page.
The solution is represented by the list of positions (a pair of integers) the horse goes through.
The possible movements of the horse from one position are described by the rewrite rules:
rules for pair[int,int] x,y : int; z : pair[int,int]; l : list; global  1st(z.l) => z end [range_rule] [x,y] => [x+2,y-1] if x+2<4 and y-1>0 end [range_rule] [x,y] => [x+2,y+1] if x+2<4 and y+1<5 end [range_rule] [x,y] => [x-2,y-1] if x-2>0 and y-1>0 end [range_rule] [x,y] => [x-2,y+1] if x-2>0 and y+1<5 end [range_rule] [x,y] => [x-1,y-2] if x-1>0 and y-2>0 end [range_rule] [x,y] => [x+1,y+2] if x+1<4 and y+2<5 end [range_rule] [x,y] => [x-1,y+2] if x-1>0 and y+2<5 end [range_rule] [x,y] => [x+1,y-2] if x+1<4 and y-2>0 end endWe use a strategy that tries to move the horse such that it is not in contradiction with the previous movements. For this we use an auxiliary function that tests if the movement we want to do at the current step does not place the horse on a previously used position (we test that the current position is different from all the positions already used).
rules for bool x,y,u,v : int; d : pair[int,int]; l : list; global  noattack(d,nil) => true end  noattack([x,y],[u,v].l) => (x!=u or y!=v) and noattack([x,y],l) end endThe rewrite rule horse_n tries to do one of the eight possible movements of the horse (given by the rules range_rule) starting from the current position and test if the new position has not been already used.
rules for list n : int; x : pair[int,int]; ql : list; local [horse_0] horse(0) => [1,1].nil end [horse_n] horse(n) => x . ql if n>0 where ql:=(horse_strat) horse(n-1) where x:=(range)1st(ql) if noattack(x,ql) end endThe strategy used to guide this rule is:
strategies for list implicit  horse_strat => dc one(horse_0 || horse_n) end endWe try to apply the rule queensrule until we get a valid placement or all the positions movements have been tried. If at one stage of the algorithm none of the position is acceptable that we get back to the previous position(s) and we try the next possible position. Once all the positions have been used we return the solution(s).