author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 66453 | cc19f7ca2ed6 |
child 69605 | a96320074298 |
permissions | -rw-r--r-- |
34965 | 1 |
theory MutabelleExtra |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63167
diff
changeset
|
2 |
imports Complex_Main "HOL-Library.Refute" |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
3 |
(* "~/repos/afp/thys/AVL-Trees/AVL" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
4 |
"~/repos/afp/thys/BinarySearchTree/BinaryTree" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
5 |
"~/repos/afp/thys/Huffman/Huffman" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
6 |
"~/repos/afp/thys/List-Index/List_Index" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
7 |
"~/repos/afp/thys/Matrix/Matrix" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
8 |
"~/repos/afp/thys/NormByEval/NBE" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
9 |
"~/repos/afp/thys/Polynomials/Polynomial" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
10 |
"~/repos/afp/thys/Presburger-Automata/Presburger_Automata" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
11 |
"~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*) |
34965 | 12 |
begin |
13 |
||
48891 | 14 |
ML_file "mutabelle.ML" |
15 |
ML_file "mutabelle_extra.ML" |
|
16 |
||
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
17 |
|
63167 | 18 |
section \<open>configuration\<close> |
34965 | 19 |
|
63167 | 20 |
ML \<open>val log_directory = ""\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
21 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
22 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
23 |
quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000] |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
24 |
|
34965 | 25 |
(* |
56850 | 26 |
nitpick_params [timeout = 5, sat_solver = MiniSat_JNI, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12] |
34965 | 27 |
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat] |
28 |
*) |
|
29 |
||
63167 | 30 |
ML \<open>val mtds = [ |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
31 |
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random", |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
32 |
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random", |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
33 |
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small", |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
34 |
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
35 |
] |
63167 | 36 |
\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
37 |
|
63167 | 38 |
ML \<open> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
39 |
fun mutation_testing_of (name, thy) = |
56147 | 40 |
(MutabelleExtra.init_random 1.0; |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
41 |
MutabelleExtra.thms_of false thy |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
42 |
|> MutabelleExtra.take_random 200 |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
43 |
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report |
69597 | 44 |
\<^theory> (1, 50) mtds thms (log_directory ^ "/" ^ name))) |
63167 | 45 |
\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
46 |
|
34965 | 47 |
|
63167 | 48 |
text \<open>Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main.\<close> |
34965 | 49 |
|
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
50 |
(* |
34965 | 51 |
ML {* |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
52 |
|
56147 | 53 |
MutabelleExtra.init_random 1.0; |
34965 | 54 |
MutabelleExtra.thms_of true @{theory Complex_Main} |
55 |
|> MutabelleExtra.take_random 1000000 |
|
56 |
|> (fn thms => List.drop (thms, 1000)) |
|
57 |
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report |
|
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
58 |
@{theory} [ |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
59 |
MutabelleExtra.quickcheck_mtd "code", |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
60 |
MutabelleExtra.smallcheck_mtd |
34965 | 61 |
(*MutabelleExtra.refute_mtd, |
62 |
MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out") |
|
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
63 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
64 |
*} |
34965 | 65 |
*) |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
66 |
|
63167 | 67 |
section \<open>Mutation testing Isabelle theories\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
68 |
|
63167 | 69 |
subsection \<open>List theory\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
70 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
71 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
72 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
73 |
mutation_testing_of ("List", @{theory List}) |
34965 | 74 |
*} |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
75 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
76 |
|
63167 | 77 |
section \<open>Mutation testing AFP theories\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
78 |
|
63167 | 79 |
subsection \<open>AVL-Trees\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
80 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
81 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
82 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
83 |
mutation_testing_of ("AVL-Trees", @{theory AVL}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
84 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
85 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
86 |
|
63167 | 87 |
subsection \<open>BinaryTree\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
88 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
89 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
90 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
91 |
mutation_testing_of ("BinaryTree", @{theory BinaryTree}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
92 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
93 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
94 |
|
63167 | 95 |
subsection \<open>Huffman\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
96 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
97 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
98 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
99 |
mutation_testing_of ("Huffman", @{theory Huffman}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
100 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
101 |
*) |
34965 | 102 |
|
63167 | 103 |
subsection \<open>List_Index\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
104 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
105 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
106 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
107 |
mutation_testing_of ("List_Index", @{theory List_Index}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
108 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
109 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
110 |
|
63167 | 111 |
subsection \<open>Matrix\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
112 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
113 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
114 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
115 |
mutation_testing_of ("Matrix", @{theory Matrix}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
116 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
117 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
118 |
|
63167 | 119 |
subsection \<open>NBE\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
120 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
121 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
122 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
123 |
mutation_testing_of ("NBE", @{theory NBE}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
124 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
125 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
126 |
|
63167 | 127 |
subsection \<open>Polynomial\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
128 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
129 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
130 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
131 |
mutation_testing_of ("Polynomial", @{theory Polynomial}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
132 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
133 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
134 |
|
63167 | 135 |
subsection \<open>Presburger Automata\<close> |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
136 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
137 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
138 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
139 |
mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
140 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
141 |
*) |
34965 | 142 |
|
39324
05452dd66b2b
finished renaming "Auto_Counterexample" to "Auto_Tools"
blanchet
parents:
34965
diff
changeset
|
143 |
end |