author | blanchet |

Tue Aug 03 17:43:15 2010 +0200 (2010-08-03) | |

changeset 38185 | b51677438b3a |

parent 38184 | 6a221fffbc8a |

child 38186 | c28018f5a1d6 |

speed up Nitpick examples a little bit

1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Aug 03 17:29:54 2010 +0200 1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Aug 03 17:43:15 2010 +0200 1.3 @@ -11,8 +11,8 @@ 1.4 imports Main 1.5 begin 1.6 1.7 -nitpick_params [unary_ints, max_potential = 0, sat_solver = MiniSat_JNI, 1.8 - max_threads = 1, timeout = 60 s] 1.9 +nitpick_params [card = 1\<midarrow>6, unary_ints, max_potential = 0, 1.10 + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] 1.11 1.12 subsection {* Curry in a Hurry *} 1.13

2.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue Aug 03 17:29:54 2010 +0200 2.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue Aug 03 17:43:15 2010 +0200 2.3 @@ -11,8 +11,8 @@ 2.4 imports Main 2.5 begin 2.6 2.7 -nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, 2.8 - timeout = 60 s] 2.9 +nitpick_params [card = 1\<midarrow>8, max_potential = 0, 2.10 + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] 2.11 2.12 primrec rot where 2.13 "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |

3.1 --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Tue Aug 03 17:29:54 2010 +0200 3.2 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Tue Aug 03 17:43:15 2010 +0200 3.3 @@ -52,7 +52,7 @@ 3.4 theorem safe: "s \<in> reach \<Longrightarrow> safe s r \<Longrightarrow> g \<in> isin s r \<Longrightarrow> owns s r = Some g" 3.5 nitpick [card room = 1, card guest = 2, card "guest option" = 3, 3.6 card key = 4, card state = 6, expect = genuine] 3.7 -nitpick [card room = 1, card guest = 2, expect = genuine] 3.8 +(* nitpick [card room = 1, card guest = 2, expect = genuine] *) 3.9 oops 3.10 3.11 end

4.1 --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Aug 03 17:29:54 2010 +0200 4.2 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Aug 03 17:43:15 2010 +0200 4.3 @@ -11,7 +11,8 @@ 4.4 imports Main 4.5 begin 4.6 4.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] 4.8 +nitpick_params [card = 1\<midarrow>6, bits = 1,2,3,4,6,8, 4.9 + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] 4.10 4.11 inductive p1 :: "nat \<Rightarrow> bool" where 4.12 "p1 0" |

5.1 --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Aug 03 17:29:54 2010 +0200 5.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Aug 03 17:43:15 2010 +0200 5.3 @@ -11,8 +11,8 @@ 5.4 imports Nitpick 5.5 begin 5.6 5.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s, 5.8 - card = 1\<midarrow>6, bits = 1,2,3,4,6,8] 5.9 +nitpick_params [card = 1\<midarrow>6, bits = 1,2,3,4,6,8, 5.10 + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] 5.11 5.12 lemma "Suc x = x + 1" 5.13 nitpick [unary_ints, expect = none]

6.1 --- a/src/HOL/Nitpick_Examples/Record_Nits.thy Tue Aug 03 17:29:54 2010 +0200 6.2 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Tue Aug 03 17:43:15 2010 +0200 6.3 @@ -11,8 +11,8 @@ 6.4 imports Main 6.5 begin 6.6 6.7 -nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, 6.8 - timeout = 60 s] 6.9 +nitpick_params [card = 1\<midarrow>6, max_potential = 0, 6.10 + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] 6.11 6.12 record point2d = 6.13 xc :: int

7.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Aug 03 17:29:54 2010 +0200 7.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Aug 03 17:43:15 2010 +0200 7.3 @@ -11,8 +11,8 @@ 7.4 imports Main 7.5 begin 7.6 7.7 -nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, 7.8 - timeout = 60 s] 7.9 +nitpick_params [card = 1\<midarrow>6, max_potential = 0, 7.10 + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] 7.11 7.12 lemma "P \<and> Q" 7.13 apply (rule conjI)