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

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