speed up Nitpick examples a little bit
authorblanchet
Tue Aug 03 17:43:15 2010 +0200 (2010-08-03)
changeset 38185b51677438b3a
parent 38184 6a221fffbc8a
child 38186 c28018f5a1d6
speed up Nitpick examples a little bit
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Datatype_Nits.thy
src/HOL/Nitpick_Examples/Hotel_Nits.thy
src/HOL/Nitpick_Examples/Induct_Nits.thy
src/HOL/Nitpick_Examples/Integer_Nits.thy
src/HOL/Nitpick_Examples/Record_Nits.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
     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)