diff --git a/Sudoku/SudokuEvent.mch b/Sudoku/SudokuEvent.mch
index cefcf11348febd0d15eaeb22897e750e0a2b9f90..87514f55fc86335e4ca17cfa575a4a9c0327ddf5 100644
--- a/Sudoku/SudokuEvent.mch
+++ b/Sudoku/SudokuEvent.mch
@@ -29,51 +29,35 @@ DEFINITIONS
MAX_OPERATIONS_SetBoard == 10;
/* PUZZLE CONSTRAINTS : */
- PUZZLE(BOARD) == (
+ PUZZLE1 ==
+ {(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),
+ (2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),
+ (3↦{(3↦6),(4↦8),(8↦1),(9↦2)}),
+ (4↦{(1↦2),(4↦3),(7↦8),(8↦5),(9↦1)}),
+ (5↦{(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(3↦8),(6↦9),(7↦3),(8↦6)}),
+ (7↦{(1↦1),(2↦9),(6↦7),(8↦8)}),
+ (8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),
+ (9↦{(3↦5),(7↦1)})}
+ ;
+ PUZZLE2 ==
+ {(1↦{(1↦1),(2↦3),(4↦8),(5↦6),(6↦5),(9↦9)}),
+ (2↦{(3↦8),(6↦4),(7↦1),(9↦2)}),
+ (3↦{(4↦1),(5↦2)}),
+ (4↦{(3↦7),(4↦6),(7↦9),(9↦3)}),
+ (5↦{(1↦9),(2↦1),(3↦5),(4↦4),(8↦8),(9↦7)}),
+ (6↦{(1↦6),(3↦3),(5↦1),(6↦7),(8↦5)}),
+ (7↦{(7↦3),(8↦4),(9↦5)}),
+ (8↦{(3↦6),(4↦7),(6↦3),(7↦8),(8↦9)}),
+ (9↦{(3↦9),(5↦8),(9↦6)})};
- BOARD(1)(1)=7 & BOARD(1)(2)=8 & BOARD(1)(3)=1 & BOARD(1)(4)=6 & BOARD(1)(6)=2
- & BOARD(1)(7)=9 & BOARD(1)(9)=5 &
- BOARD(2)(1)=9 & BOARD(2)(3)=2 & BOARD(2)(4)=7 & BOARD(2)(5)=1 &
- BOARD(3)(3)=6 & BOARD(3)(4)=8 & BOARD(3)(8)=1 & BOARD(3)(9)=2 &
-
- BOARD(4)(1)=2 & BOARD(4)(4)=3 & BOARD(4)(7)=8 & BOARD(4)(8)=5 & BOARD(4)(9)=1 &
- BOARD(5)(2)=7 & BOARD(5)(3)=3 & BOARD(5)(4)=5 & BOARD(5)(9)=4 &
- BOARD(6)(3)=8 & BOARD(6)(6)=9 & BOARD(6)(7)=3 & BOARD(6)(8)=6 &
-
- BOARD(7)(1)=1 & BOARD(7)(2)=9 & BOARD(7)(6)=7 & BOARD(7)(8)=8 &
- BOARD(8)(1)=8 & BOARD(8)(2)=6 & BOARD(8)(3)=7 & BOARD(8)(6)=3 & BOARD(8)(7)=4 & BOARD(8)(9)=9 &
- BOARD(9)(3)=5 & BOARD(9)(7)=1
- );
- PUZZLE2(BOARD) == (
-
- BOARD(1)(1)=1 & BOARD(1)(2)=3 & BOARD(1)(4)=8 & BOARD(1)(5)=6 & BOARD(1)(6)=5
- & BOARD(1)(9)=9 &
- BOARD(2)(3)=8 & BOARD(2)(6)=4 & BOARD(2)(7)=1 & BOARD(2)(9)=2 &
- BOARD(3)(4)=1 & BOARD(3)(5)=2 &
-
- BOARD(4)(3)=7 & BOARD(4)(4)=6 & BOARD(4)(7)=9 & BOARD(4)(9)=3 &
- BOARD(5)(1)=9 & BOARD(5)(2)=1 & BOARD(5)(3)=5 & BOARD(5)(4)=4
- & BOARD(5)(8)=8 & BOARD(5)(9)=7 &
- BOARD(6)(1)=6 & BOARD(6)(3)=3 & BOARD(6)(5)=1 & BOARD(6)(6)=7 & BOARD(6)(8)=5 &
-
- BOARD(7)(7)=3 & BOARD(7)(8)=4 & BOARD(7)(9)=5 &
- BOARD(8)(3)=6 & BOARD(8)(4)=7 & BOARD(8)(6)=3 & BOARD(8)(7)=8 & BOARD(8)(8)=9 &
- BOARD(9)(3)=9 & BOARD(9)(5)=8 & BOARD(9)(9)=6
- );
-
- PUZZLE3(BOARD) == (
- BOARD(1)(2)=4 & BOARD(1)(3)=3 & BOARD(1)(6)=5 & BOARD(1)(8)=8 & BOARD(1)(9)=7 &
- BOARD(2)(2)=9 & BOARD(2)(6)=3 &
- BOARD(3)(5)=2 & BOARD(3)(8)=1 &
-
- BOARD(4)(3)=9 & BOARD(4)(4)=8 & BOARD(4)(9)=5 &
- BOARD(5)(2)=5 & BOARD(5)(3)=8 & BOARD(5)(8)=2 & BOARD(5)(9)=6 &
- BOARD(6)(2)=7 & BOARD(6)(4)=2 &
-
- BOARD(7)(1)=5 & BOARD(7)(2)=8 & BOARD(7)(4)=1 & BOARD(7)(6)=2 & BOARD(7)(7)=4 & BOARD (7)(8)=7 &
- BOARD(8)(9)=3 &
- BOARD(9)(1)=9 & BOARD(9)(2)=1 & BOARD(9)(4)=7 & BOARD(9)(5)=6 & BOARD(9)(7)=5
- );
+ PUZZLE3 ==
+ {(1↦{(2↦4),(3↦3),(6↦5),(8↦8),(9↦7)}),
+ (2↦{(2↦9),(6↦3)}),(3↦{(5↦2),(8↦1)}),(4↦{(3↦9),(4↦8),(9↦5)}),
+ (5↦{(2↦5),(3↦8),(8↦2),(9↦6)}),
+ (6↦{(2↦7),(4↦2)}),
+ (7↦{(1↦5),(2↦8),(4↦1),(6↦2),(7↦4),(8↦7)}),
+ (8↦{(9↦3)}),(9↦{(1↦9),(2↦1),(4↦7),(5↦6),(7↦5)})}
+ ;
UnassignedPosition(x,y) == x:DOM & y:DOM & not(y:dom(Board(x)));
PossibleVals(cx,cy) == DOM \ ran({x,y,r| x|->y : conflict_pos(cx,cy) & y:dom(Board(x)) & r=Board(x)(y)})
@@ -84,7 +68,7 @@ CONSTANTS
PuzzleBoard /*@desc "Stored Puzzle" */
PROPERTIES
PuzzleBoard : DOM --> (DOM +-> RAN) &
- PUZZLE(PuzzleBoard) &
+ PuzzleBoard : {PUZZLE1,PUZZLE2,PUZZLE3} &
get_square = %x.(x:DOM | 1 + (x-1)/3) /*@desc "Get square (1,2,3) for a coordinate 1..9" */
&
conflict_pos = %(x,y).(x:DOM & y:DOM | {x2,y2 | x2:DOM & y2:DOM & (x,y) /= (x2,y2) &