--- 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
--- 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 =
--- 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."