restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
1.1 --- a/NEWS Sun Jun 03 15:49:55 2012 +0200
1.2 +++ b/NEWS Mon Jun 04 09:07:23 2012 +0200
1.3 @@ -25,6 +25,12 @@
1.4 It is switched on by default, and can be switched off by setting
1.5 the configuration quickcheck_optimise_equality to false.
1.6
1.7 +* The SMT solver Z3 has now by default a restricted set of directly
1.8 +supported features. For the full set of features (div/mod, nonlinear
1.9 +arithmetic, datatypes/records) with potential proof reconstruction
1.10 +failures, enable the configuration option "z3_with_extensions".
1.11 +Minor INCOMPATIBILITY.
1.12 +
1.13 New in Isabelle2012 (May 2012)
1.14 ------------------------------
1.15
2.1 --- a/src/HOL/Boogie/Examples/VCC_Max.thy Sun Jun 03 15:49:55 2012 +0200
2.2 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy Mon Jun 04 09:07:23 2012 +0200
2.3 @@ -50,6 +50,7 @@
2.4 declare [[smt_certificates = "VCC_Max.certs"]]
2.5 declare [[smt_read_only_certificates = true]]
2.6 declare [[smt_oracle = false]]
2.7 +declare [[z3_with_extensions = true]]
2.8
2.9 boogie_status
2.10
3.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy Sun Jun 03 15:49:55 2012 +0200
3.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Jun 04 09:07:23 2012 +0200
3.3 @@ -2319,7 +2319,7 @@
3.4 note ab = conjunctD2[OF this[unfolded Un_subset_iff]]
3.5 guess w1 using B(2)[OF ab(1)] .. note w1=conjunctD2[OF this]
3.6 guess w2 using B(4)[OF ab(2)] .. note w2=conjunctD2[OF this]
3.7 - have *:"\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False" by smt
3.8 + have *:"\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False" using [[z3_with_extensions]] by smt
3.9 note le_less_trans[OF component_le_norm[of _ k]] note this[OF w1(2)] this[OF w2(2)] moreover
3.10 have "w1$$k \<le> w2$$k" apply(rule lem[OF w1(1) w2(1)]) using assms by auto ultimately
3.11 show False unfolding euclidean_simps by(rule *) qed
3.12 @@ -3050,7 +3050,7 @@
3.13 hence "d \<in> {a..b}" using s(2)[OF k(1)] unfolding k by auto note di = this[unfolded mem_interval,THEN spec[where x=i]]
3.14 hence xyi:"y$$i \<noteq> x$$i" unfolding y_def unfolding i xi euclidean_lambda_beta'[OF i(2)] if_P[OF refl]
3.15 apply(cases) apply(subst if_P,assumption) unfolding if_not_P not_le using as(2)
3.16 - using assms(2)[unfolded content_eq_0] using i(2) by smt+
3.17 + using assms(2)[unfolded content_eq_0] using i(2) using [[z3_with_extensions]] by smt+
3.18 thus "y \<noteq> x" unfolding euclidean_eq[where 'a='a] using i by auto
3.19 have *:"{..<DIM('a)} = insert i ({..<DIM('a)} - {i})" using i by auto
3.20 have "norm (y - x) < e + setsum (\<lambda>i. 0) {..<DIM('a)}" apply(rule le_less_trans[OF norm_le_l1])
3.21 @@ -4236,7 +4236,7 @@
3.22 proof- fix a b c d::"'n::ordered_euclidean_space" assume as:"ball 0 (max B1 B2) \<subseteq> {a..b}" "ball 0 (max B1 B2) \<subseteq> {c..d}"
3.23 have **:"ball 0 B1 \<subseteq> ball (0::'n::ordered_euclidean_space) (max B1 B2)" "ball 0 B2 \<subseteq> ball (0::'n::ordered_euclidean_space) (max B1 B2)" by auto
3.24 have *:"\<And>ga gc ha hc fa fc::real. abs(ga - i) < e / 3 \<and> abs(gc - i) < e / 3 \<and> abs(ha - j) < e / 3 \<and>
3.25 - abs(hc - j) < e / 3 \<and> abs(i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc\<Longrightarrow> abs(fa - fc) < e" by smt
3.26 + abs(hc - j) < e / 3 \<and> abs(i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc\<Longrightarrow> abs(fa - fc) < e" using [[z3_with_extensions]] by smt
3.27 show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - integral {c..d} (\<lambda>x. if x \<in> s then f x else 0)) < e"
3.28 unfolding real_norm_def apply(rule *, safe) unfolding real_norm_def[THEN sym]
3.29 apply(rule B1(2),rule order_trans,rule **,rule as(1))
4.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy Sun Jun 03 15:49:55 2012 +0200
4.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy Mon Jun 04 09:07:23 2012 +0200
4.3 @@ -327,9 +327,13 @@
4.4
4.5 lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P" by smt
4.6
4.7 -lemma "x + (let y = x mod 2 in 2 * y + 1) \<ge> x + (1::int)" by smt
4.8 +lemma "x + (let y = x mod 2 in 2 * y + 1) \<ge> x + (1::int)"
4.9 + using [[z3_with_extensions]]
4.10 + by smt
4.11
4.12 -lemma "x + (let y = x mod 2 in y + y) < x + (3::int)" by smt
4.13 +lemma "x + (let y = x mod 2 in y + y) < x + (3::int)"
4.14 + using [[z3_with_extensions]]
4.15 + by smt
4.16
4.17 lemma
4.18 assumes "x \<noteq> (0::real)"
4.19 @@ -339,7 +343,7 @@
4.20 lemma
4.21 assumes "(n + m) mod 2 = 0" and "n mod 4 = 3"
4.22 shows "n mod 2 = 1 & m mod 2 = (1::int)"
4.23 - using assms by smt
4.24 + using assms [[z3_with_extensions]] by smt
4.25
4.26
4.27
4.28 @@ -393,18 +397,21 @@
4.29 subsection {* Non-linear arithmetic over integers and reals *}
4.30
4.31 lemma "a > (0::int) \<Longrightarrow> a*b > 0 \<Longrightarrow> b > 0"
4.32 - using [[smt_oracle=true]]
4.33 + using [[smt_oracle, z3_with_extensions]]
4.34 by smt
4.35
4.36 lemma "(a::int) * (x + 1 + y) = a * x + a * (y + 1)"
4.37 + using [[z3_with_extensions]]
4.38 by smt
4.39
4.40 lemma "((x::real) * (1 + y) - x * (1 - y)) = (2 * x * y)"
4.41 + using [[z3_with_extensions]]
4.42 by smt
4.43
4.44 lemma
4.45 "(U::int) + (1 + p) * (b + e) + p * d =
4.46 U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
4.47 + using [[z3_with_extensions]]
4.48 by smt
4.49
4.50 lemma [z3_rule]:
4.51 @@ -413,7 +420,9 @@
4.52 shows False
4.53 using assms by (metis mult_le_0_iff)
4.54
4.55 -lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0" by smt
4.56 +lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0"
4.57 + using [[z3_with_extensions]]
4.58 + by smt
4.59
4.60
4.61
4.62 @@ -498,6 +507,7 @@
4.63 eval_dioph ks (map (\<lambda>x. x div 2) xs) =
4.64 (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
4.65 using [[smt_oracle=true]] (*FIXME*)
4.66 + using [[z3_with_extensions]]
4.67 by (smt eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
4.68
4.69
5.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy Sun Jun 03 15:49:55 2012 +0200
5.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy Mon Jun 04 09:07:23 2012 +0200
5.3 @@ -315,6 +315,7 @@
5.4 "(3::nat) div 3 = 1"
5.5 "(x::nat) div 3 \<le> x"
5.6 "(x div 3 = x) = (x = 0)"
5.7 + using [[z3_with_extensions]]
5.8 by smt+
5.9
5.10 lemma
5.11 @@ -329,11 +330,13 @@
5.12 "(3::nat) mod 3 = 0"
5.13 "x mod 3 < 3"
5.14 "(x mod 3 = x) = (x < 3)"
5.15 + using [[z3_with_extensions]]
5.16 by smt+
5.17
5.18 lemma
5.19 "(x::nat) = x div 1 * 1 + x mod 1"
5.20 "x = x div 3 * 3 + x mod 3"
5.21 + using [[z3_with_extensions]]
5.22 by smt+
5.23
5.24 lemma
5.25 @@ -447,6 +450,7 @@
5.26 "(-1::int) div -3 = 0"
5.27 "(-3::int) div -3 = 1"
5.28 "(-5::int) div -3 = 1"
5.29 + using [[z3_with_extensions]]
5.30 by smt+
5.31
5.32 lemma
5.33 @@ -476,11 +480,13 @@
5.34 "(-5::int) mod -3 = -2"
5.35 "x mod 3 < 3"
5.36 "(x mod 3 = x) \<longrightarrow> (x < 3)"
5.37 + using [[z3_with_extensions]]
5.38 by smt+
5.39
5.40 lemma
5.41 "(x::int) = x div 1 * 1 + x mod 1"
5.42 "x = x div 3 * 3 + x mod 3"
5.43 + using [[z3_with_extensions]]
5.44 by smt+
5.45
5.46 lemma
5.47 @@ -585,6 +591,7 @@
5.48 "(x::real) / 1 = x"
5.49 "x > 0 \<longrightarrow> x / 3 < x"
5.50 "x < 0 \<longrightarrow> x / 3 > x"
5.51 + using [[z3_with_extensions]]
5.52 by smt+
5.53
5.54 lemma
5.55 @@ -592,6 +599,7 @@
5.56 "(x * 3) / 3 = x"
5.57 "x > 0 \<longrightarrow> 2 * x / 3 < x"
5.58 "x < 0 \<longrightarrow> 2 * x / 3 > x"
5.59 + using [[z3_with_extensions]]
5.60 by smt+
5.61
5.62 lemma
5.63 @@ -793,7 +801,7 @@
5.64 "(fst (x, y) = snd (x, y)) = (x = y)"
5.65 "(fst p = snd p) = (p = (snd p, fst p))"
5.66 using fst_conv snd_conv pair_collapse
5.67 - using [[smt_datatypes, smt_oracle]]
5.68 + using [[smt_datatypes, smt_oracle, z3_with_extensions]]
5.69 by smt+
5.70
5.71 lemma
5.72 @@ -807,14 +815,14 @@
5.73 "hd (tl [x, y, z]) = y"
5.74 "tl (tl [x, y, z]) = [z]"
5.75 using hd.simps tl.simps(2)
5.76 - using [[smt_datatypes, smt_oracle]]
5.77 + using [[smt_datatypes, smt_oracle, z3_with_extensions]]
5.78 by smt+
5.79
5.80 lemma
5.81 "fst (hd [(a, b)]) = a"
5.82 "snd (hd [(a, b)]) = b"
5.83 using fst_conv snd_conv pair_collapse hd.simps tl.simps(2)
5.84 - using [[smt_datatypes, smt_oracle]]
5.85 + using [[smt_datatypes, smt_oracle, z3_with_extensions]]
5.86 by smt+
5.87
5.88
5.89 @@ -826,7 +834,7 @@
5.90 "cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2"
5.91 "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2"
5.92 using point.simps
5.93 - using [[smt_datatypes, smt_oracle]]
5.94 + using [[smt_datatypes, smt_oracle, z3_with_extensions]]
5.95 using [[z3_options="AUTO_CONFIG=false"]]
5.96 by smt+
5.97
5.98 @@ -839,7 +847,7 @@
5.99 "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
5.100 "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p"
5.101 using point.simps
5.102 - using [[smt_datatypes, smt_oracle]]
5.103 + using [[smt_datatypes, smt_oracle, z3_with_extensions]]
5.104 using [[z3_options="AUTO_CONFIG=false"]]
5.105 by smt+
5.106
5.107 @@ -848,7 +856,7 @@
5.108 "cx (p \<lparr> cy := a \<rparr>) = cx p"
5.109 "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>"
5.110 using point.simps
5.111 - using [[smt_datatypes, smt_oracle]]
5.112 + using [[smt_datatypes, smt_oracle, z3_with_extensions]]
5.113 using [[z3_options="AUTO_CONFIG=false"]]
5.114 by smt+
5.115
5.116 @@ -860,7 +868,7 @@
5.117 "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2"
5.118 "black p1 \<noteq> black p2 \<longrightarrow> p1 \<noteq> p2"
5.119 using point.simps bw_point.simps
5.120 - using [[smt_datatypes, smt_oracle]]
5.121 + using [[smt_datatypes, smt_oracle, z3_with_extensions]]
5.122 by smt+
5.123
5.124 lemma
5.125 @@ -877,7 +885,7 @@
5.126 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
5.127 p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
5.128 using point.simps bw_point.simps
5.129 - using [[smt_datatypes, smt_oracle]]
5.130 + using [[smt_datatypes, smt_oracle, z3_with_extensions]]
5.131 using [[z3_options="AUTO_CONFIG=false"]]
5.132 by smt+
5.133
5.134 @@ -891,7 +899,7 @@
5.135 "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> =
5.136 p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>"
5.137 using point.simps bw_point.simps
5.138 - using [[smt_datatypes, smt_oracle]]
5.139 + using [[smt_datatypes, smt_oracle, z3_with_extensions]]
5.140 using [[z3_options="AUTO_CONFIG=false"]]
5.141 by smt
5.142
5.143 @@ -905,7 +913,7 @@
5.144 "nplus n1 n1 = n2"
5.145 "nplus n1 n2 = n3"
5.146 using n1_def n2_def n3_def nplus_def
5.147 - using [[smt_datatypes, smt_oracle]]
5.148 + using [[smt_datatypes, smt_oracle, z3_with_extensions]]
5.149 using [[z3_options="AUTO_CONFIG=false"]]
5.150 by smt+
5.151
6.1 --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Sun Jun 03 15:49:55 2012 +0200
6.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Mon Jun 04 09:07:23 2012 +0200
6.3 @@ -11,6 +11,7 @@
6.4 Z3_Non_Commercial_Accepted |
6.5 Z3_Non_Commercial_Declined
6.6 val z3_non_commercial: unit -> z3_non_commercial
6.7 + val z3_with_extensions: bool Config.T
6.8 val setup: theory -> theory
6.9 end
6.10
6.11 @@ -133,6 +134,9 @@
6.12 end
6.13
6.14
6.15 +val z3_with_extensions =
6.16 + Attrib.setup_config_bool @{binding z3_with_extensions} (K false)
6.17 +
6.18 local
6.19 fun z3_make_command is_remote name () =
6.20 if_z3_non_commercial (make_command is_remote name)
6.21 @@ -163,11 +167,8 @@
6.22 handle SMT_Failure.SMT _ => outcome (swap o split_last)
6.23 end
6.24
6.25 - val with_extensions =
6.26 - Attrib.setup_config_bool @{binding z3_with_extensions} (K true)
6.27 -
6.28 fun select_class ctxt =
6.29 - if Config.get ctxt with_extensions then Z3_Interface.smtlib_z3C
6.30 + if Config.get ctxt z3_with_extensions then Z3_Interface.smtlib_z3C
6.31 else SMTLIB_Interface.smtlibC
6.32
6.33 fun mk is_remote = {