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"
authorboehmes
Mon Jun 04 09:07:23 2012 +0200 (2012-06-04)
changeset 48069e9b2782c4f99
parent 48068 04aeda922be2
child 48071 d7864276bca8
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"
NEWS
src/HOL/Boogie/Examples/VCC_Max.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/Tools/SMT/smt_setup_solvers.ML
     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 = {