example tweaking -- also prevents Nitpick_Tests from using more than 1 thread
authorblanchet
Tue Aug 03 18:14:44 2010 +0200 (2010-08-03)
changeset 38186c28018f5a1d6
parent 38185 b51677438b3a
child 38187 fd28328daf73
example tweaking -- also prevents Nitpick_Tests from using more than 1 thread
src/HOL/Nitpick_Examples/Induct_Nits.thy
src/HOL/Tools/Nitpick/nitpick_scope.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
     1.1 --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue Aug 03 17:43:15 2010 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue Aug 03 18:14:44 2010 +0200
     1.3 @@ -11,8 +11,8 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -nitpick_params [card = 1\<midarrow>6,  bits = 1,2,3,4,6,8,
     1.8 -                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
     1.9 +nitpick_params [card = 1\<midarrow>8, unary_ints, sat_solver = MiniSat_JNI,
    1.10 +                max_threads = 1, timeout = 60 s]
    1.11  
    1.12  inductive p1 :: "nat \<Rightarrow> bool" where
    1.13  "p1 0" |
    1.14 @@ -115,58 +115,42 @@
    1.15  
    1.16  lemma "p3 = q3"
    1.17  nitpick [expect = none]
    1.18 -nitpick [dont_star_linear_preds, expect = none]
    1.19 -nitpick [non_wf, expect = potential]
    1.20 -nitpick [non_wf, dont_box, expect = none]
    1.21 -nitpick [non_wf, dont_star_linear_preds, expect = none]
    1.22 +nitpick [non_wf, expect = none]
    1.23  sorry
    1.24  
    1.25  lemma "p4 = q4"
    1.26  nitpick [expect = none]
    1.27 -nitpick [dont_star_linear_preds, expect = none]
    1.28 -nitpick [non_wf, expect = potential]
    1.29 -nitpick [non_wf, dont_box, expect = none]
    1.30 -nitpick [non_wf, dont_star_linear_preds, expect = none]
    1.31 +nitpick [non_wf, expect = none]
    1.32  sorry
    1.33  
    1.34  lemma "p3 = UNIV - p4"
    1.35  nitpick [expect = none]
    1.36 -nitpick [dont_star_linear_preds, expect = none]
    1.37 -nitpick [non_wf, expect = potential]
    1.38 -nitpick [non_wf, dont_box, expect = none]
    1.39 -nitpick [non_wf, dont_star_linear_preds, expect = none]
    1.40 +nitpick [non_wf, expect = none]
    1.41  sorry
    1.42  
    1.43  lemma "q3 = UNIV - q4"
    1.44  nitpick [expect = none]
    1.45 -nitpick [dont_star_linear_preds, expect = none]
    1.46  nitpick [non_wf, expect = none]
    1.47 -nitpick [non_wf, dont_box, expect = none]
    1.48 -nitpick [non_wf, dont_star_linear_preds, expect = none]
    1.49  sorry
    1.50  
    1.51  lemma "p3 \<inter> q4 \<noteq> {}"
    1.52  nitpick [expect = potential]
    1.53  nitpick [non_wf, expect = potential]
    1.54 -nitpick [non_wf, dont_star_linear_preds, expect = potential]
    1.55  sorry
    1.56  
    1.57  lemma "q3 \<inter> p4 \<noteq> {}"
    1.58  nitpick [expect = potential]
    1.59  nitpick [non_wf, expect = potential]
    1.60 -nitpick [non_wf, dont_star_linear_preds, expect = potential]
    1.61  sorry
    1.62  
    1.63  lemma "p3 \<union> q4 \<noteq> UNIV"
    1.64  nitpick [expect = potential]
    1.65  nitpick [non_wf, expect = potential]
    1.66 -nitpick [non_wf, dont_star_linear_preds, expect = potential]
    1.67  sorry
    1.68  
    1.69  lemma "q3 \<union> p4 \<noteq> UNIV"
    1.70  nitpick [expect = potential]
    1.71  nitpick [non_wf, expect = potential]
    1.72 -nitpick [non_wf, dont_star_linear_preds, expect = potential]
    1.73  sorry
    1.74  
    1.75  end
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Aug 03 17:43:15 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Aug 03 18:14:44 2010 +0200
     2.3 @@ -272,27 +272,20 @@
     2.4    in mono_block :: nonmono_blocks end
     2.5  
     2.6  val sync_threshold = 5
     2.7 +val linearity = 5
     2.8  
     2.9 -fun all_combinations_ordered_smartly ks =
    2.10 +val all_combinations_ordered_smartly =
    2.11    let
    2.12 -    fun cost_with_monos [] = 0
    2.13 -      | cost_with_monos (k :: ks) =
    2.14 +    fun cost [] = 0
    2.15 +      | cost [k] = k
    2.16 +      | cost (k :: ks) =
    2.17          if k < sync_threshold andalso forall (curry (op =) k) ks then
    2.18            k - sync_threshold
    2.19          else
    2.20 -          k * (k + 1) div 2 + Integer.sum ks
    2.21 -    fun cost_without_monos [] = 0
    2.22 -      | cost_without_monos [k] = k
    2.23 -      | cost_without_monos (_ :: k :: ks) =
    2.24 -        if k < sync_threshold andalso forall (curry (op =) k) ks then
    2.25 -          k - sync_threshold
    2.26 -        else
    2.27 -          Integer.sum (k :: ks)
    2.28 +          Integer.product (map (fn k => (k + linearity) * (k + linearity))
    2.29 +                               (k :: ks))
    2.30    in
    2.31 -    ks |> all_combinations
    2.32 -       |> map (`(if fst (hd ks) > 1 then cost_with_monos
    2.33 -                 else cost_without_monos))
    2.34 -       |> sort (int_ord o pairself fst) |> map snd
    2.35 +    all_combinations #> map cost #> sort (int_ord o pairself fst) #> map snd
    2.36    end
    2.37  
    2.38  fun is_self_recursive_constr_type T =
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Aug 03 17:43:15 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Aug 03 18:14:44 2010 +0200
     3.3 @@ -318,8 +318,13 @@
     3.4    end
     3.5  
     3.6  fun run_all_tests () =
     3.7 -  case Kodkod.solve_any_problem false NONE 0 1
     3.8 -                                (map (problem_for_nut @{context}) tests) of
     3.9 +  let
    3.10 +    val {overlord, ...} = Nitpick_Isar.default_params thy []
    3.11 +    val max_threads = 1
    3.12 +    val max_solutions = 1
    3.13 +  in
    3.14 +    case Kodkod.solve_any_problem overlord NONE max_threads max_solutions
    3.15 +                                  (map (problem_for_nut @{context}) tests) of
    3.16      Kodkod.Normal ([], _, _) => ()
    3.17    | _ => error "Tests failed."
    3.18