compile + reduce problem size by a notch
authorblanchet
Sat Dec 21 09:44:30 2013 +0100 (2013-12-21)
changeset 5484510df188349b3
parent 54844 630ba4d8a206
child 54846 bf86b2002c96
compile + reduce problem size by a notch
src/HOL/Nitpick_Examples/Mini_Nits.thy
src/HOL/Nitpick_Examples/minipick.ML
     1.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Sat Dec 21 09:44:30 2013 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Sat Dec 21 09:44:30 2013 +0100
     1.3 @@ -13,9 +13,8 @@
     1.4  
     1.5  ML_file "minipick.ML"
     1.6  
     1.7 -nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1]
     1.8 -
     1.9 -nitpick_params [total_consts = smart]
    1.10 +nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
    1.11 +  total_consts = smart]
    1.12  
    1.13  ML {*
    1.14  val check = Minipick.minipick @{context}
    1.15 @@ -34,8 +33,8 @@
    1.16  ML_val {* genuine 1 @{prop False} *}
    1.17  ML_val {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
    1.18  ML_val {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
    1.19 -ML_val {* none 5 @{prop "\<forall>x. x = x"} *}
    1.20 -ML_val {* none 5 @{prop "\<exists>x. x = x"} *}
    1.21 +ML_val {* none 4 @{prop "\<forall>x. x = x"} *}
    1.22 +ML_val {* none 4 @{prop "\<exists>x. x = x"} *}
    1.23  ML_val {* none 1 @{prop "\<forall>x. x = y"} *}
    1.24  ML_val {* genuine 2 @{prop "\<forall>x. x = y"} *}
    1.25  ML_val {* none 2 @{prop "\<exists>x. x = y"} *}
    1.26 @@ -47,10 +46,10 @@
    1.27  ML_val {* genuine 2 @{prop "All = Ex"} *}
    1.28  ML_val {* none 1 @{prop "All P = Ex P"} *}
    1.29  ML_val {* genuine 2 @{prop "All P = Ex P"} *}
    1.30 -ML_val {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
    1.31 -ML_val {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
    1.32 +ML_val {* none 4 @{prop "x = y \<longrightarrow> P x = P y"} *}
    1.33 +ML_val {* none 4 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
    1.34  ML_val {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
    1.35 -ML_val {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
    1.36 +ML_val {* none 4 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
    1.37  ML_val {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
    1.38  ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
    1.39  ML_val {* genuine 1 @{prop "(op =) X = Ex"} *}
    1.40 @@ -64,49 +63,49 @@
    1.41  ML_val {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
    1.42  ML_val {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
    1.43  ML_val {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
    1.44 -ML_val {* none 5 @{prop "{a} = {a, a}"} *}
    1.45 +ML_val {* none 4 @{prop "{a} = {a, a}"} *}
    1.46  ML_val {* genuine 2 @{prop "{a} = {a, b}"} *}
    1.47  ML_val {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
    1.48 -ML_val {* none 5 @{prop "{}\<^sup>+ = {}"} *}
    1.49 -ML_val {* none 5 @{prop "UNIV\<^sup>+ = UNIV"} *}
    1.50 -ML_val {* none 5 @{prop "(UNIV \<Colon> ('a \<times> 'b) set) - {} = UNIV"} *}
    1.51 -ML_val {* none 5 @{prop "{} - (UNIV \<Colon> ('a \<times> 'b) set) = {}"} *}
    1.52 +ML_val {* none 4 @{prop "{}\<^sup>+ = {}"} *}
    1.53 +ML_val {* none 4 @{prop "UNIV\<^sup>+ = UNIV"} *}
    1.54 +ML_val {* none 4 @{prop "(UNIV \<Colon> ('a \<times> 'b) set) - {} = UNIV"} *}
    1.55 +ML_val {* none 4 @{prop "{} - (UNIV \<Colon> ('a \<times> 'b) set) = {}"} *}
    1.56  ML_val {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.57  ML_val {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.58 -ML_val {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.59 -ML_val {* none 5 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"} *}
    1.60 -ML_val {* none 5 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"} *}
    1.61 -ML_val {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
    1.62 -ML_val {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
    1.63 +ML_val {* none 4 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.64 +ML_val {* none 4 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"} *}
    1.65 +ML_val {* none 4 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"} *}
    1.66 +ML_val {* none 4 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
    1.67 +ML_val {* none 4 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
    1.68  ML_val {* genuine 2 @{prop "(a, b) = (b, a)"} *}
    1.69  ML_val {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
    1.70 -ML_val {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
    1.71 +ML_val {* none 4 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
    1.72  ML_val {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
    1.73 -ML_val {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
    1.74 +ML_val {* none 4 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
    1.75  ML_val {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
    1.76 -ML_val {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
    1.77 +ML_val {* none 4 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
    1.78  ML_val {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
    1.79 -ML_val {* none 5 @{prop "fst (a, b) = a"} *}
    1.80 +ML_val {* none 4 @{prop "fst (a, b) = a"} *}
    1.81  ML_val {* none 1 @{prop "fst (a, b) = b"} *}
    1.82  ML_val {* genuine 2 @{prop "fst (a, b) = b"} *}
    1.83  ML_val {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
    1.84  ML_val {* genuine 2 @{prop "f ((x, z), y) = (x, z)"} *}
    1.85  ML_val {* none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"} *}
    1.86 -ML_val {* none 5 @{prop "snd (a, b) = b"} *}
    1.87 +ML_val {* none 4 @{prop "snd (a, b) = b"} *}
    1.88  ML_val {* none 1 @{prop "snd (a, b) = a"} *}
    1.89  ML_val {* genuine 2 @{prop "snd (a, b) = a"} *}
    1.90  ML_val {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
    1.91  ML_val {* genuine 1 @{prop P} *}
    1.92  ML_val {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
    1.93  ML_val {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
    1.94 -ML_val {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
    1.95 +ML_val {* none 4 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
    1.96  ML_val {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
    1.97  ML_val {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
    1.98  ML_val {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
    1.99  ML_val {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
   1.100 -ML_val {* none 5 @{prop "f = (\<lambda>x. f x)"} *}
   1.101 -ML_val {* none 5 @{prop "f = (\<lambda>x. f x\<Colon>'a \<Rightarrow> bool)"} *}
   1.102 -ML_val {* none 5 @{prop "f = (\<lambda>x y. f x y)"} *}
   1.103 -ML_val {* none 5 @{prop "f = (\<lambda>x y. f x y\<Colon>'a \<Rightarrow> bool)"} *}
   1.104 +ML_val {* none 4 @{prop "f = (\<lambda>x. f x)"} *}
   1.105 +ML_val {* none 4 @{prop "f = (\<lambda>x. f x\<Colon>'a \<Rightarrow> bool)"} *}
   1.106 +ML_val {* none 4 @{prop "f = (\<lambda>x y. f x y)"} *}
   1.107 +ML_val {* none 4 @{prop "f = (\<lambda>x y. f x y\<Colon>'a \<Rightarrow> bool)"} *}
   1.108  
   1.109  end
     2.1 --- a/src/HOL/Nitpick_Examples/minipick.ML	Sat Dec 21 09:44:30 2013 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/minipick.ML	Sat Dec 21 09:44:30 2013 +0100
     2.3 @@ -429,11 +429,11 @@
     2.4  
     2.5  fun solve_any_kodkod_problem thy problems =
     2.6    let
     2.7 -    val {debug, overlord, ...} = Nitpick_Isar.default_params thy []
     2.8 +    val {debug, overlord, timeout, ...} = Nitpick_Isar.default_params thy []
     2.9      val max_threads = 1
    2.10      val max_solutions = 1
    2.11    in
    2.12 -    case solve_any_problem debug overlord NONE max_threads max_solutions
    2.13 +    case solve_any_problem debug overlord timeout max_threads max_solutions
    2.14                             problems of
    2.15        JavaNotFound => "unknown"
    2.16      | JavaTooOld => "unknown"