extraction: no more OCaml code for map.Map

sudoku example now uses arrays only
parent e4746a0b
......@@ -1199,7 +1199,7 @@ clean::
# Ocaml realizations
#######################
OCAMLLIBS_FILES = why3__BigInt why3__IntAux why3__Array why3__Map
OCAMLLIBS_FILES = why3__BigInt why3__IntAux why3__Array
OCAMLLIBS_MODULES := $(addprefix lib/ocaml/, $(OCAMLLIBS_FILES))
......
......@@ -128,17 +128,6 @@ theory list.Combine
syntax function combine "(List.combine %1 %2)"
end
(* map *)
theory map.Map
syntax type map "((%1, %2) Why3__Map.map)"
syntax function const "(Why3__Map.const %1)"
syntax function ([]) "(Why3__Map.get %1 %2)"
syntax function get "(Why3__Map.get %1 %2)"
syntax function ([<-]) "(Why3__Map.set %1 %2 %3)"
syntax function set "(Why3__Map.set %1 %2 %3)"
end
(* WhyML *)
module ref.Ref
......
(** {1 An Efficient Sudoku Solver } *)
(** {1 An Efficient Sudoku Solver }
Author: Claude Marché (Inria)
Guillaume Melquiond (Inria) *)
(** {2 A theory of 9x9 grids} *)
module Grid
module Grid
use import int.Int
use import map.Map
......@@ -115,7 +118,7 @@ module Grid
(** [included g1 g2] *)
predicate included (g1 g2 : grid) =
forall i : int. is_index i /\ 1 <= Map.get g1 i <= 9 ->
forall i : int. is_index i /\ 1 <= Map.get g1 i <= 9 ->
Map.get g2 i = Map.get g1 i
(** validity is monotonic w.r.t. inclusion *)
......@@ -126,7 +129,7 @@ module Grid
valid_chunk g i s o
lemma subset_valid :
forall s g h.
forall s g h.
well_formed_sudoku s /\ included g h /\ valid s h -> valid s g
(** A solution of a grid [data] is a full grid [sol]
......@@ -145,78 +148,78 @@ module TheClassicalSudokuGrid
use import map.Map
use import int.Int
constant c_start : map int int
= (const (-1))
[ 0<-0][ 1<-1][ 2<-2][ 3<-3][ 4<-4][ 5<-5][ 6<-6][ 7<-7][ 8<-8]
[ 9<-0][10<-1][11<-2][12<-3][13<-4][14<-5][15<-6][16<-7][17<-8]
[18<-0][19<-1][20<-2][21<-3][22<-4][23<-5][24<-6][25<-7][26<-8]
[27<-0][28<-1][29<-2][30<-3][31<-4][32<-5][33<-6][34<-7][35<-8]
[36<-0][37<-1][38<-2][39<-3][40<-4][41<-5][42<-6][43<-7][44<-8]
[45<-0][46<-1][47<-2][48<-3][49<-4][50<-5][51<-6][52<-7][53<-8]
[54<-0][55<-1][56<-2][57<-3][58<-4][59<-5][60<-6][61<-7][62<-8]
[63<-0][64<-1][65<-2][66<-3][67<-4][68<-5][69<-6][70<-7][71<-8]
[72<-0][73<-1][74<-2][75<-3][76<-4][77<-5][78<-6][79<-7][80<-8]
constant c_offsets : map int int
= (const (-1))
[ 0<-0][ 1<-9][ 2<-18][ 3<-27][ 4<-36][ 5<-45][ 6<-54][ 7<-63][ 8<-72]
constant r_start : map int int
= (const (-1))
[ 0<- 0][ 1<- 0][ 2<- 0][ 3<- 0][ 4<- 0][ 5<- 0][ 6<- 0][ 7<- 0][ 8<- 0]
[ 9<- 9][10<- 9][11<- 9][12<- 9][13<- 9][14<- 9][15<- 9][16<- 9][17<- 9]
[18<-18][19<-18][20<-18][21<-18][22<-18][23<-18][24<-18][25<-18][26<-18]
[27<-27][28<-27][29<-27][30<-27][31<-27][32<-27][33<-27][34<-27][35<-27]
[36<-36][37<-36][38<-36][39<-36][40<-36][41<-36][42<-36][43<-36][44<-36]
[45<-45][46<-45][47<-45][48<-45][49<-45][50<-45][51<-45][52<-45][53<-45]
[54<-54][55<-54][56<-54][57<-54][58<-54][59<-54][60<-54][61<-54][62<-54]
[63<-63][64<-63][65<-63][66<-63][67<-63][68<-63][69<-63][70<-63][71<-63]
[72<-72][73<-72][74<-72][75<-72][76<-72][77<-72][78<-72][79<-72][80<-72]
constant r_offsets : map int int
= (const (-1))
[ 0<-0][ 1<-1][ 2<-2][ 3<-3][ 4<-4][ 5<-5][ 6<-6][ 7<-7][ 8<-8]
constant s_start : map int int
= (const (-1))
[ 0<- 0][ 1<- 0][ 2<- 0][ 3<- 3][ 4<- 3][ 5<- 3][ 6<- 6][ 7<- 6][ 8<- 6]
[ 9<- 0][10<- 0][11<- 0][12<- 3][13<- 3][14<- 3][15<- 6][16<- 6][17<- 6]
[18<- 0][19<- 0][20<- 0][21<- 3][22<- 3][23<- 3][24<- 6][25<- 6][26<- 6]
[27<-27][28<-27][29<-27][30<-30][31<-30][32<-30][33<-33][34<-33][35<-33]
[36<-27][37<-27][38<-27][39<-30][40<-30][41<-30][42<-33][43<-33][44<-33]
[45<-27][46<-27][47<-27][48<-30][49<-30][50<-30][51<-33][52<-33][53<-33]
[54<-54][55<-54][56<-54][57<-57][58<-57][59<-57][60<-60][61<-60][62<-60]
[63<-54][64<-54][65<-54][66<-57][67<-57][68<-57][69<-60][70<-60][71<-60]
[72<-54][73<-54][74<-54][75<-57][76<-57][77<-57][78<-60][79<-60][80<-60]
constant s_offsets : map int int
= (const (-1))
[ 0<-0][ 1<-1][ 2<-2][ 3<-9][ 4<-10][ 5<-11][ 6<-18][ 7<-19][ 8<-20]
use import array.Array
let array_from_map (n:int) (m:map int int) : array int
requires { n >= 0 }
ensures { result.length = n }
ensures { forall i. 0 <= i < n -> result[i] = Map.get m i }
=
let r = Array.make n 0 in
for j = 0 to n-1 do
invariant { forall i. 0 <= i < j -> r[i] = Map.get m i }
r[j] <- Map.get m j
done;
r
let classical_sudoku () : sudoku_chunks
ensures { well_formed_sudoku result }
=
{ column_start = array_from_map 81 c_start;
column_offsets = array_from_map 9 c_offsets;
row_start = array_from_map 81 r_start ;
row_offsets = array_from_map 9 r_offsets ;
square_start = array_from_map 81 s_start ;
square_offsets = array_from_map 9 s_offsets ;
}
(* column start *)
let cs = Array.make 81 0 in
cs[ 0]<-0; cs[ 1]<-1; cs[ 2]<-2; cs[ 3]<-3; cs[ 4]<-4; cs[ 5]<-5;
cs[ 6]<-6; cs[ 7]<-7; cs[ 8]<-8; cs[ 9]<-0; cs[10]<-1; cs[11]<-2;
cs[12]<-3; cs[13]<-4; cs[14]<-5; cs[15]<-6; cs[16]<-7; cs[17]<-8;
cs[18]<-0; cs[19]<-1; cs[20]<-2; cs[21]<-3; cs[22]<-4; cs[23]<-5;
cs[24]<-6; cs[25]<-7; cs[26]<-8; cs[27]<-0; cs[28]<-1; cs[29]<-2;
cs[30]<-3; cs[31]<-4; cs[32]<-5; cs[33]<-6; cs[34]<-7; cs[35]<-8;
cs[36]<-0; cs[37]<-1; cs[38]<-2; cs[39]<-3; cs[40]<-4; cs[41]<-5;
cs[42]<-6; cs[43]<-7; cs[44]<-8; cs[45]<-0; cs[46]<-1; cs[47]<-2;
cs[48]<-3; cs[49]<-4; cs[50]<-5; cs[51]<-6; cs[52]<-7; cs[53]<-8;
cs[54]<-0; cs[55]<-1; cs[56]<-2; cs[57]<-3; cs[58]<-4; cs[59]<-5;
cs[60]<-6; cs[61]<-7; cs[62]<-8; cs[63]<-0; cs[64]<-1; cs[65]<-2;
cs[66]<-3; cs[67]<-4; cs[68]<-5; cs[69]<-6; cs[70]<-7; cs[71]<-8;
cs[72]<-0; cs[73]<-1; cs[74]<-2; cs[75]<-3; cs[76]<-4; cs[77]<-5;
cs[78]<-6; cs[79]<-7; cs[80]<-8;
(* column offset *)
let co = Array.make 9 0 in
co[ 0]<-0; co[ 1]<-9; co[ 2]<-18; co[ 3]<-27; co[ 4]<-36; co[
5]<-45; co[ 6]<-54; co[ 7]<-63; co[ 8]<-72;
(* row start *)
let rs = Array.make 81 0 in
rs[ 0]<- 0; rs[ 1]<- 0; rs[ 2]<- 0; rs[ 3]<- 0; rs[ 4]<-0; rs[5]<-0;
rs[ 6]<- 0; rs[ 7]<- 0; rs[ 8]<- 0; rs[ 9]<- 9; rs[10]<-9; rs[11]<-9;
rs[12]<- 9; rs[13]<- 9; rs[14]<- 9; rs[15]<- 9; rs[16]<-9; rs[17]<-9;
rs[18]<-18; rs[19]<-18; rs[20]<-18; rs[21]<-18; rs[22]<-18;
rs[23]<-18; rs[24]<-18; rs[25]<-18; rs[26]<-18; rs[27]<-27;
rs[28]<-27; rs[29]<-27; rs[30]<-27; rs[31]<-27; rs[32]<-27;
rs[33]<-27; rs[34]<-27; rs[35]<-27; rs[36]<-36; rs[37]<-36;
rs[38]<-36; rs[39]<-36; rs[40]<-36; rs[41]<-36; rs[42]<-36;
rs[43]<-36; rs[44]<-36; rs[45]<-45; rs[46]<-45; rs[47]<-45;
rs[48]<-45; rs[49]<-45; rs[50]<-45; rs[51]<-45; rs[52]<-45;
rs[53]<-45; rs[54]<-54; rs[55]<-54; rs[56]<-54; rs[57]<-54;
rs[58]<-54; rs[59]<-54; rs[60]<-54; rs[61]<-54; rs[62]<-54;
rs[63]<-63; rs[64]<-63; rs[65]<-63; rs[66]<-63; rs[67]<-63;
rs[68]<-63; rs[69]<-63; rs[70]<-63; rs[71]<-63; rs[72]<-72;
rs[73]<-72; rs[74]<-72; rs[75]<-72; rs[76]<-72; rs[77]<-72;
rs[78]<-72; rs[79]<-72; rs[80]<-72;
(* row offset *)
let ro = Array.make 9 0 in
ro[ 0]<-0; ro[ 1]<-1; ro[ 2]<-2; ro[ 3]<-3; ro[ 4]<-4; ro[ 5]<-5;
ro[ 6]<-6; ro[ 7]<-7; ro[ 8]<-8;
(* square start *)
let ss = Array.make 81 0 in
ss[ 0]<- 0; ss[ 1]<- 0; ss[ 2]<- 0; ss[ 3]<- 3; ss[ 4]<- 3;
ss[ 5]<- 3; ss[ 6]<- 6; ss[ 7]<- 6; ss[ 8]<- 6; ss[ 9]<- 0;
ss[10]<- 0; ss[11]<- 0; ss[12]<- 3; ss[13]<- 3; ss[14]<- 3; ss[15]<- 6;
ss[16]<- 6; ss[17]<- 6; ss[18]<- 0; ss[19]<- 0; ss[20]<- 0;
ss[21]<- 3; ss[22]<- 3; ss[23]<- 3; ss[24]<- 6; ss[25]<- 6;
ss[26]<- 6; ss[27]<-27; ss[28]<-27; ss[29]<-27; ss[30]<-30;
ss[31]<-30; ss[32]<-30; ss[33]<-33; ss[34]<-33; ss[35]<-33;
ss[36]<-27; ss[37]<-27; ss[38]<-27; ss[39]<-30; ss[40]<-30;
ss[41]<-30; ss[42]<-33; ss[43]<-33; ss[44]<-33; ss[45]<-27;
ss[46]<-27; ss[47]<-27; ss[48]<-30; ss[49]<-30; ss[50]<-30;
ss[51]<-33; ss[52]<-33; ss[53]<-33; ss[54]<-54; ss[55]<-54;
ss[56]<-54; ss[57]<-57; ss[58]<-57; ss[59]<-57; ss[60]<-60;
ss[61]<-60; ss[62]<-60; ss[63]<-54; ss[64]<-54; ss[65]<-54;
ss[66]<-57; ss[67]<-57; ss[68]<-57; ss[69]<-60; ss[70]<-60;
ss[71]<-60; ss[72]<-54; ss[73]<-54; ss[74]<-54; ss[75]<-57;
ss[76]<-57; ss[77]<-57; ss[78]<-60; ss[79]<-60; ss[80]<-60;
(* square offset *)
let so = Array.make 9 0 in
so[ 0]<-0; so[ 1]<-1; so[ 2]<-2; so[ 3]<-9; so[ 4]<-10;
so[ 5]<-11; so[ 6]<-18; so[ 7]<-19; so[ 8]<-20;
{ column_start = cs; column_offsets = co;
row_start = rs; row_offsets = ro;
square_start = ss; square_offsets = so; }
end
......@@ -230,7 +233,7 @@ module Solver
use import array.Array
use import int.Int
(** predicate for the loop invariant of next function *)
(** predicate for the loop invariant of next function *)
predicate valid_chunk_up_to (g:grid) (i:int)
(start:array int) (offsets:array int) (off:int) =
let s = start[i] in
......@@ -238,7 +241,7 @@ module Solver
0 <= o1 < off /\ 0 <= o2 < off /\ o1 <> o2 ->
let i1 = s + offsets[o1] in
let i2 = s + offsets[o2] in
1 <= Map.get g i1 <= 9 /\ 1 <= Map.get g i2 <= 9 ->
1 <= Map.get g i1 <= 9 /\ 1 <= Map.get g i2 <= 9 ->
Map.get g i1 <> Map.get g i2
exception Invalid
......@@ -275,7 +278,7 @@ module Solver
end
done
(** predicate for the loop invariant of next function *)
(** predicate for the loop invariant of next function *)
predicate valid_up_to (s:sudoku_chunks) (g:grid) (i:int) =
forall j : int. 0 <= j < i ->
valid_column s g j /\ valid_row s g j /\ valid_square s g j
......@@ -300,7 +303,7 @@ module Solver
end
(** [full_up_to g i] is true when all cells [0..i-1] in grid [g] are
non empty *)
non empty *)
predicate full_up_to (g : grid) (i : int) = forall j :
int. 0 <= j < i -> 1 <= Map.get g j <= 9
......@@ -387,7 +390,7 @@ this is true but with 2 different possible reasons:
is_index i /\ valid_up_to s g i /\ 1 <= x <= 9 /\
valid_column s (Map.set g i x) i /\
valid_row s (Map.set g i x) i /\
valid_square s (Map.set g i x) i
valid_square s (Map.set g i x) i
-> valid_up_to s (Map.set g i x) (i+1)
......@@ -436,10 +439,10 @@ this is true but with 2 different possible reasons:
assert { let grid' = Map.set (at g 'L).elts i k in
grid_eq grid' g.elts &&
valid_chunk grid' i s.column_start s.column_offsets &&
valid_chunk grid' i s.row_start s.row_offsets &&
valid_chunk grid' i s.row_start s.row_offsets &&
valid_chunk grid' i s.square_start s.square_offsets &&
valid_up_to s grid' (i+1) };
assert { valid_up_to s g.elts (i+1) };
valid_up_to s grid' (i+1) };
assert { valid_up_to s g.elts (i+1) };
solve_aux s g (i + 1)
with Invalid ->
assert { (* for completeness *)
......
......@@ -16,7 +16,7 @@ ifeq ($(BENCH),yes)
endif
MAIN = main
OBJ = sudoku__Grid sudoku__TheClassicalSudokuGrid sudoku__Solver
OBJ = map__Map sudoku__Grid sudoku__TheClassicalSudokuGrid sudoku__Solver
ML = $(addsuffix .ml, $(OBJ))
CMO = $(addsuffix .cmo, $(OBJ))
......
......@@ -28,948 +28,186 @@
<theory
name="Grid"
locfile="../sudoku.mlw"
loclnum="7" loccnumb="7" loccnume="11"
loclnum="10" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="grid_eq_sub"
locfile="../sudoku.mlw"
loclnum="28" loccnumb="8" loccnume="19"
sum="fdcfcaf0fdf16dd242d8dfc17c7d4e55"
proved="true"
expanded="false"
shape="agrid_eq_subV0V1V2V3Iagrid_eqV0V1Aainfix &lt;=V3c81Aainfix &lt;=c0V3Aainfix &lt;=V2c81Aainfix &lt;=c0V2F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="subset_valid_chunk"
locfile="../sudoku.mlw"
loclnum="122" loccnumb="8" loccnume="26"
sum="c4024f04874718a237e221e417edd967"
proved="true"
expanded="false"
shape="avalid_chunkV0V2V3V4Iavalid_chunkV1V2V3V4Aachunk_valid_indexesV3V4Aais_indexV2FIaincludedV0V1F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="subset_valid"
locfile="../sudoku.mlw"
loclnum="128" loccnumb="8" loccnume="20"
sum="c261153d98ca30c10c8e94db4827abcf"
proved="true"
expanded="false"
shape="avalidV0V1IavalidV0V2AaincludedV1V2Aawell_formed_sudokuV0F">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.70"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.32"/>
</proof>
</goal>
</theory>
<theory
name="TheClassicalSudokuGrid"
locfile="../sudoku.mlw"
loclnum="142" loccnumb="7" loccnume="29"
verified="true"
expanded="true">
<goal
name="WP_parameter array_from_map"
locfile="../sudoku.mlw"
loclnum="198" loccnumb="6" loccnume="20"
expl="VC for array_from_map"
sum="72930ca0f6fb50b182cea3ce43d2eb1d"
proved="true"
expanded="false"
shape="ainfix =agetV3V4agetV1V4Iainfix &lt;V4V0Aainfix &lt;=c0V4FAainfix &lt;=c0V0Iainfix =agetV3V5agetV1V5Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=c0V5FAainfix =agetV7V8agetV1V8Iainfix &lt;V8ainfix +V6c1Aainfix &lt;=c0V8FIainfix =V7asetV3V6agetV1V6Aainfix &lt;=c0V0FAainfix &lt;V6V0Aainfix &lt;=c0V6Aainfix &lt;=c0V0Iainfix =agetV3V9agetV1V9Iainfix &lt;V9V6Aainfix &lt;=c0V9FIainfix &lt;=V6V2Aainfix &lt;=c0V6FFAainfix =agetaconstc0V10agetV1V10Iainfix &lt;V10c0Aainfix &lt;=c0V10FIainfix &lt;=c0V2Aainfix =agetaconstc0V11agetV1V11Iainfix &lt;V11V0Aainfix &lt;=c0V11FIainfix &gt;c0V2Lainfix -V0c1Iainfix &lt;=c0V0Aainfix &gt;=V0c0Iainfix &gt;=V0c0F">
<label
name="expl:VC for array_from_map"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter array_from_map.1"
locfile="../sudoku.mlw"
loclnum="198" loccnumb="6" loccnume="20"
expl="1. array creation size"
sum="0670e628128fb973755715cf7d3ba7a9"
proved="true"
expanded="false"
shape="array creation sizeainfix &gt;=V0c0Iainfix &gt;=V0c0F">
<label
name="expl:VC for array_from_map"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter array_from_map.2"
locfile="../sudoku.mlw"
loclnum="198" loccnumb="6" loccnume="20"
expl="2. postcondition"
sum="f53331f3554d0b16b680c7d1653e551d"
proved="true"
expanded="false"
shape="postconditionainfix =agetaconstc0V3agetV1V3Iainfix &lt;V3V0Aainfix &lt;=c0V3FIainfix &gt;c0V2Lainfix -V0c1Iainfix &lt;=c0V0Iainfix &gt;=V0c0Iainfix &gt;=V0c0F">
<label
name="expl:VC for array_from_map"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter array_from_map.3"
locfile="../sudoku.mlw"
loclnum="198" loccnumb="6" loccnume="20"
expl="3. loop invariant init"
sum="21dd4c5b5d4efd7842316e1f380958fd"
proved="true"
expanded="false"
shape="loop invariant initainfix =agetaconstc0V3agetV1V3Iainfix &lt;V3c0Aainfix &lt;=c0V3FIainfix &lt;=c0V2Lainfix -V0c1Iainfix &lt;=c0V0Iainfix &gt;=V0c0Iainfix &gt;=V0c0F">
<label
name="expl:VC for array_from_map"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter array_from_map.4"
locfile="../sudoku.mlw"
loclnum="198" loccnumb="6" loccnume="20"
expl="4. type invariant"
sum="13b04f934002cfed71710f1a0cf3485a"
proved="true"
expanded="false"
shape="type invariantainfix &lt;=c0V0Iainfix =agetV3V5agetV1V5Iainfix &lt;V5V4Aainfix &lt;=c0V5FIainfix &lt;=V4V2Aainfix &lt;=c0V4FFIainfix &lt;=c0V2Lainfix -V0c1Iainfix &lt;=c0V0Iainfix &gt;=V0c0Iainfix &gt;=V0c0F">
<label
name="expl:VC for array_from_map"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter array_from_map.5"
locfile="../sudoku.mlw"
loclnum="198" loccnumb="6" loccnume="20"
expl="5. index in array bounds"
sum="687df4b9c6e2bcc996d67d3fabc1dcfc"
proved="true"
expanded="false"
shape="index in array boundsainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;=c0V0Iainfix =agetV3V5agetV1V5Iainfix &lt;V5V4Aainfix &lt;=c0V5FIainfix &lt;=V4V2Aainfix &lt;=c0V4FFIainfix &lt;=c0V2Lainfix -V0c1Iainfix &lt;=c0V0Iainfix &gt;=V0c0Iainfix &gt;=V0c0F">
<label
name="expl:VC for array_from_map"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter array_from_map.6"
locfile="../sudoku.mlw"
loclnum="198" loccnumb="6" loccnume="20"
expl="6. loop invariant preservation"
sum="fa386656ecaa783426548f9b8282bafc"
proved="true"
expanded="false"
shape="loop invariant preservationainfix =agetV5V6agetV1V6Iainfix &lt;V6ainfix +V4c1Aainfix &lt;=c0V6FIainfix =V5asetV3V4agetV1V4Aainfix &lt;=c0V0FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix =agetV3V7agetV1V7Iainfix &lt;V7V4Aainfix &lt;=c0V7FIainfix &lt;=V4V2Aainfix &lt;=c0V4FFIainfix &lt;=c0V2Lainfix -V0c1Iainfix &lt;=c0V0Iainfix &gt;=V0c0Iainfix &gt;=V0c0F">
<label
name="expl:VC for array_from_map"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter array_from_map.7"
locfile="../sudoku.mlw"
loclnum="198" loccnumb="6" loccnume="20"
expl="7. type invariant"
sum="ebb6a0a4dee89f732575b27632ad0b49"
proved="true"
expanded="false"
shape="type invariantainfix &lt;=c0V0Iainfix =agetV3V4agetV1V4Iainfix &lt;V4ainfix +V2c1Aainfix &lt;=c0V4FFIainfix &lt;=c0V2Lainfix -V0c1Iainfix &lt;=c0V0Iainfix &gt;=V0c0Iainfix &gt;=V0c0F">
<label
name="expl:VC for array_from_map"/>
<proof
prover="0"
timelimit="5"