# HG changeset patch
# User blanchet
# Date 1280852084 -7200
# Node ID c28018f5a1d657611c267ffe168210af30a225b8
# Parent  b51677438b3aa66936f913675fab6b822f9f89c4
example tweaking -- also prevents Nitpick_Tests from using more than 1 thread

diff -r b51677438b3a -r c28018f5a1d6 src/HOL/Nitpick_Examples/Induct_Nits.thy
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue Aug 03 17:43:15 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue Aug 03 18:14:44 2010 +0200
@@ -11,8 +11,8 @@
 imports Main
 begin
 
-nitpick_params [card = 1\<midarrow>6,  bits = 1,2,3,4,6,8,
-                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+nitpick_params [card = 1\<midarrow>8, unary_ints, sat_solver = MiniSat_JNI,
+                max_threads = 1, timeout = 60 s]
 
 inductive p1 :: "nat \<Rightarrow> bool" where
 "p1 0" |
@@ -115,58 +115,42 @@
 
 lemma "p3 = q3"
 nitpick [expect = none]
-nitpick [dont_star_linear_preds, expect = none]
-nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_box, expect = none]
-nitpick [non_wf, dont_star_linear_preds, expect = none]
+nitpick [non_wf, expect = none]
 sorry
 
 lemma "p4 = q4"
 nitpick [expect = none]
-nitpick [dont_star_linear_preds, expect = none]
-nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_box, expect = none]
-nitpick [non_wf, dont_star_linear_preds, expect = none]
+nitpick [non_wf, expect = none]
 sorry
 
 lemma "p3 = UNIV - p4"
 nitpick [expect = none]
-nitpick [dont_star_linear_preds, expect = none]
-nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_box, expect = none]
-nitpick [non_wf, dont_star_linear_preds, expect = none]
+nitpick [non_wf, expect = none]
 sorry
 
 lemma "q3 = UNIV - q4"
 nitpick [expect = none]
-nitpick [dont_star_linear_preds, expect = none]
 nitpick [non_wf, expect = none]
-nitpick [non_wf, dont_box, expect = none]
-nitpick [non_wf, dont_star_linear_preds, expect = none]
 sorry
 
 lemma "p3 \<inter> q4 \<noteq> {}"
 nitpick [expect = potential]
 nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_star_linear_preds, expect = potential]
 sorry
 
 lemma "q3 \<inter> p4 \<noteq> {}"
 nitpick [expect = potential]
 nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_star_linear_preds, expect = potential]
 sorry
 
 lemma "p3 \<union> q4 \<noteq> UNIV"
 nitpick [expect = potential]
 nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_star_linear_preds, expect = potential]
 sorry
 
 lemma "q3 \<union> p4 \<noteq> UNIV"
 nitpick [expect = potential]
 nitpick [non_wf, expect = potential]
-nitpick [non_wf, dont_star_linear_preds, expect = potential]
 sorry
 
 end
diff -r b51677438b3a -r c28018f5a1d6 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Aug 03 17:43:15 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Aug 03 18:14:44 2010 +0200
@@ -272,27 +272,20 @@
   in mono_block :: nonmono_blocks end
 
 val sync_threshold = 5
+val linearity = 5
 
-fun all_combinations_ordered_smartly ks =
+val all_combinations_ordered_smartly =
   let
-    fun cost_with_monos [] = 0
-      | cost_with_monos (k :: ks) =
+    fun cost [] = 0
+      | cost [k] = k
+      | cost (k :: ks) =
         if k < sync_threshold andalso forall (curry (op =) k) ks then
           k - sync_threshold
         else
-          k * (k + 1) div 2 + Integer.sum ks
-    fun cost_without_monos [] = 0
-      | cost_without_monos [k] = k
-      | cost_without_monos (_ :: k :: ks) =
-        if k < sync_threshold andalso forall (curry (op =) k) ks then
-          k - sync_threshold
-        else
-          Integer.sum (k :: ks)
+          Integer.product (map (fn k => (k + linearity) * (k + linearity))
+                               (k :: ks))
   in
-    ks |> all_combinations
-       |> map (`(if fst (hd ks) > 1 then cost_with_monos
-                 else cost_without_monos))
-       |> sort (int_ord o pairself fst) |> map snd
+    all_combinations #> map cost #> sort (int_ord o pairself fst) #> map snd
   end
 
 fun is_self_recursive_constr_type T =
diff -r b51677438b3a -r c28018f5a1d6 src/HOL/Tools/Nitpick/nitpick_tests.ML
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Aug 03 17:43:15 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Aug 03 18:14:44 2010 +0200
@@ -318,8 +318,13 @@
   end
 
 fun run_all_tests () =
-  case Kodkod.solve_any_problem false NONE 0 1
-                                (map (problem_for_nut @{context}) tests) of
+  let
+    val {overlord, ...} = Nitpick_Isar.default_params thy []
+    val max_threads = 1
+    val max_solutions = 1
+  in
+    case Kodkod.solve_any_problem overlord NONE max_threads max_solutions
+                                  (map (problem_for_nut @{context}) tests) of
     Kodkod.Normal ([], _, _) => ()
   | _ => error "Tests failed."