Commit 74db69c8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove some obsolete conversions between machine integers and unbounded integers.

parent 13235416
......@@ -163,7 +163,7 @@ module NQueens63
requires { 0 <= pos < (length board) }
requires { is_board board (pos + 1) }
= try
let q = ref (of_int 0) in
let q = ref 0 in
while !q < pos do
invariant { 0 <= !q <= pos }
invariant { is_board board (pos + 1) }
......@@ -173,7 +173,7 @@ module NQueens63
if bq = bpos then raise MInconsistent;
if bq - bpos = pos - !q then raise MInconsistent;
if bpos - bq = pos - !q then raise MInconsistent;
q := !q + of_int 1
q := !q + 1
done;
True
with MInconsistent ->
......@@ -193,28 +193,28 @@ module NQueens63
if pos = n then
solutions := P.succ !solutions
else
let i = ref (of_int 0) in
let i = ref 0 in
while !i < n do
invariant { 0 <= !i <= n }
invariant { is_board board (pos) }
variant { n - !i }
board[pos] <- !i;
if check_is_consistent board pos then
count_bt_queens solutions board n (pos + of_int 1);
i := !i + of_int 1
count_bt_queens solutions board n (pos + 1);
i := !i + 1
done
let count_queens (n: int63) : P.t
requires { n >= 0 }
ensures { true }
=
let solutions = ref P.zero in
let board = Array63.make n (of_int 0) in
count_bt_queens solutions board n (of_int 0);
!solutions
let solutions = ref P.zero in
let board = Array63.make n 0 in
count_bt_queens solutions board n 0;
!solutions
let test_count_8 () =
let n = of_int 8 in
let n = 8 in
count_queens n
end
......
......@@ -72,7 +72,7 @@
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC count_bt_queens" expl="VC for count_bt_queens" proved="true">
<proof prover="1"><result status="valid" time="2.13" steps="845"/></proof>
<proof prover="1"><result status="valid" time="2.13" steps="833"/></proof>
</goal>
<goal name="VC count_queens" expl="VC for count_queens" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
......@@ -81,15 +81,15 @@
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
</theory>
<theory name="NQueens63" proved="true" sum="4b8bb165ecc0921fc643db0ce5f9a72f">
<theory name="NQueens63" proved="true" sum="41b8e82a3dd96cf59d310353e9a33ac7">
<goal name="VC check_is_consistent" expl="VC for check_is_consistent" proved="true">
<proof prover="1"><result status="valid" time="0.36" steps="1142"/></proof>
<proof prover="1"><result status="valid" time="0.36" steps="1122"/></proof>
</goal>
<goal name="VC count_bt_queens" expl="VC for count_bt_queens" proved="true">
<proof prover="1"><result status="valid" time="0.88" steps="4213"/></proof>
<proof prover="1"><result status="valid" time="0.60" steps="1162"/></proof>
</goal>
<goal name="VC count_queens" expl="VC for count_queens" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC test_count_8" expl="VC for test_count_8" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment