Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
dc4c0616
Commit
dc4c0616
authored
Feb 13, 2015
by
MARCHE Claude
Browse files
Sudoku: do not use the randomized version
parent
8866bbfc
Changes
6
Hide whitespace changes
Inline
Side-by-side
drivers/ocaml-gen.drv
View file @
dc4c0616
...
...
@@ -279,4 +279,4 @@ module random.Random
syntax val random_int "Why3__BigInt.random_int"
end
\ No newline at end of file
end
examples/sudoku/Makefile
View file @
dc4c0616
...
...
@@ -20,7 +20,7 @@ ifeq ($(BENCH),yes)
endif
MAIN
=
main
GEN
=
map__Map sudoku__Grid sudoku__TheClassicalSudokuGrid sudoku__Solver
sudoku__RandomSolver
GEN
=
map__Map sudoku__Grid sudoku__TheClassicalSudokuGrid sudoku__Solver
OBJ
=
$(GEN)
GENML
=
$(
addsuffix
.ml,
$(GEN)
)
...
...
examples/sudoku/jsmain.ml
View file @
dc4c0616
...
...
@@ -107,7 +107,7 @@ let solve_board rows _ =
done
;
begin
try
let
a
=
Sudoku__
Random
Solver
.
check_then_solve
sudoku
input_grid
in
let
a
=
Sudoku__Solver
.
check_then_solve
sudoku
input_grid
in
display_sol
rows
a
with
Sudoku__Solver
.
NoSolution
->
no_sol
rows
end
;
...
...
examples/sudoku/main.ml
View file @
dc4c0616
...
...
@@ -37,7 +37,7 @@ let print_grid fmt a =
let
()
=
let
sudoku
=
Sudoku__TheClassicalSudokuGrid
.
classical_sudoku
()
in
printf
"Problem: %a@."
print_grid
input_grid
;
let
a
=
Sudoku__
Random
Solver
.
solve
sudoku
input_grid
let
a
=
Sudoku__Solver
.
solve
sudoku
input_grid
in
printf
"Solution: %a@."
print_grid
a
...
...
examples/sudoku/why3session.xml
View file @
dc4c0616
...
...
@@ -36,8 +36,8 @@
<proof
prover=
"3"
timelimit=
"6"
><result
status=
"valid"
time=
"1.06"
/></proof>
</goal>
</theory>
<theory
name=
"Solver"
sum=
"
b469e9f218362f529979b7aa8794fb40
"
expanded=
"true"
>
<goal
name=
"WP_parameter check_valid_chunk"
expl=
"VC for check_valid_chunk"
expanded=
"true"
>
<theory
name=
"Solver"
sum=
"
2ff5b0732d3f991a59fb450771ba62fb
"
expanded=
"true"
>
<goal
name=
"WP_parameter check_valid_chunk"
expl=
"VC for check_valid_chunk"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"2.59"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.81"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"3.56"
/></proof>
...
...
@@ -632,14 +632,22 @@
</goal>
</transf>
</goal>
<goal
name=
"WP_parameter solve"
expl=
"VC for solve"
expanded=
"true"
>
<goal
name=
"WP_parameter solve"
expl=
"VC for solve"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.04"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"WP_parameter check_then_solve"
expl=
"VC for check_then_solve"
expanded=
"true"
>
<goal
name=
"WP_parameter check_then_solve"
expl=
"VC for check_then_solve"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.13"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.10"
steps=
"69"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.10"
steps=
"48"
/></proof>
</goal>
</theory>
<theory
name=
"RandomSolver"
sum=
"7dbb8a684c2ba04fa97211933ee456e7"
expanded=
"true"
>
<goal
name=
"WP_parameter solve_aux"
expl=
"VC for solve_aux"
expanded=
"true"
>
</goal>
<goal
name=
"WP_parameter solve"
expl=
"VC for solve"
expanded=
"true"
>
</goal>
<goal
name=
"WP_parameter check_then_solve"
expl=
"VC for check_then_solve"
expanded=
"true"
>
</goal>
</theory>
<theory
name=
"Test"
sum=
"96bf6ded35162d43136dfbf608f579d3"
expanded=
"true"
>
...
...
examples/sudoku/why3shapes.gz
View file @
dc4c0616
No preview for this file type
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment