1.1 --- a/CONTRIBUTORS Fri Sep 18 14:40:24 2009 +0200
1.2 +++ b/CONTRIBUTORS Fri Sep 18 18:13:19 2009 +0200
1.3 @@ -7,6 +7,9 @@
1.4 Contributions to this Isabelle version
1.5 --------------------------------------
1.6
1.7 +* September 2009: Sascha Boehme, TUM
1.8 + SMT method using external SMT solvers
1.9 +
1.10 * September 2009: Florian Haftmann, TUM
1.11 Refinement of Sets and Lattices
1.12
2.1 --- a/NEWS Fri Sep 18 14:40:24 2009 +0200
2.2 +++ b/NEWS Fri Sep 18 18:13:19 2009 +0200
2.3 @@ -18,6 +18,13 @@
2.4
2.5 *** HOL ***
2.6
2.7 +* New proof method "smt" for a combination of first-order logic
2.8 +with equality, linear and nonlinear (natural/integer/real)
2.9 +arithmetic, and fixed-size bitvectors; there is also basic
2.10 +support for higher-order features (esp. lambda abstractions).
2.11 +It is an incomplete decision procedure based on external SMT
2.12 +solvers using the oracle mechanism.
2.13 +
2.14 * Reorganization of number theory:
2.15 * former session NumberTheory now named Old_Number_Theory
2.16 * new session Number_Theory by Jeremy Avigad; if possible, prefer this.
3.1 --- a/etc/components Fri Sep 18 14:40:24 2009 +0200
3.2 +++ b/etc/components Fri Sep 18 18:13:19 2009 +0200
3.3 @@ -15,3 +15,4 @@
3.4 src/HOL/Tools/ATP_Manager
3.5 src/HOL/Mirabelle
3.6 src/HOL/Library/Sum_Of_Squares
3.7 +src/HOL/SMT
4.1 --- a/src/HOL/IsaMakefile Fri Sep 18 14:40:24 2009 +0200
4.2 +++ b/src/HOL/IsaMakefile Fri Sep 18 18:13:19 2009 +0200
4.3 @@ -40,6 +40,7 @@
4.4 HOL-Prolog \
4.5 HOL-SET-Protocol \
4.6 HOL-SizeChange \
4.7 + HOL-SMT \
4.8 HOL-Statespace \
4.9 HOL-Subst \
4.10 TLA-Buffer \
4.11 @@ -1134,6 +1135,19 @@
4.12 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
4.13
4.14
4.15 +## HOL-SMT
4.16 +
4.17 +HOL-SMT: HOL-Word $(LOG)/HOL-SMT.gz
4.18 +
4.19 +$(LOG)/HOL-SMT.gz: $(OUT)/HOL-Word SMT/SMT_Definitions.thy SMT/SMT.thy \
4.20 + SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \
4.21 + SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML \
4.22 + SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML \
4.23 + SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML \
4.24 + SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML SMT/Tools/z3_model.ML
4.25 + @cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
4.26 +
4.27 +
4.28 ## clean
4.29
4.30 clean:
4.31 @@ -1156,4 +1170,4 @@
4.32 $(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz \
4.33 $(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA \
4.34 $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz \
4.35 - $(LOG)/HOL-Mirabelle.gz
4.36 + $(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-SMT.gz
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/SMT/Examples/SMT_Examples.thy Fri Sep 18 18:13:19 2009 +0200
5.3 @@ -0,0 +1,182 @@
5.4 +(* Title: SMT_Examples.thy
5.5 + Author: Sascha Böhme, TU Muenchen
5.6 +*)
5.7 +
5.8 +header {* Examples for the 'smt' tactic. *}
5.9 +
5.10 +theory SMT_Examples
5.11 +imports "../SMT"
5.12 +begin
5.13 +
5.14 +declare [[smt_solver=z3, z3_proofs=false]]
5.15 +declare [[smt_trace=true]] (*FIXME*)
5.16 +
5.17 +
5.18 +section {* Propositional and first-order logic *}
5.19 +
5.20 +lemma "True" by smt
5.21 +lemma "p \<or> \<not>p" by smt
5.22 +lemma "(p \<and> True) = p" by smt
5.23 +lemma "(p \<or> q) \<and> \<not>p \<Longrightarrow> q" by smt
5.24 +lemma "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)" by smt
5.25 +lemma "P=P=P=P=P=P=P=P=P=P" by smt
5.26 +
5.27 +axiomatization symm_f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
5.28 + symm_f: "symm_f x y = symm_f y x"
5.29 +lemma "a = a \<and> symm_f a b = symm_f b a" by (smt add: symm_f)
5.30 +
5.31 +
5.32 +section {* Linear arithmetic *}
5.33 +
5.34 +lemma "(3::int) = 3" by smt
5.35 +lemma "(3::real) = 3" by smt
5.36 +lemma "(3 :: int) + 1 = 4" by smt
5.37 +lemma "max (3::int) 8 > 5" by smt
5.38 +lemma "abs (x :: real) + abs y \<ge> abs (x + y)" by smt
5.39 +lemma "let x = (2 :: int) in x + x \<noteq> 5" by smt
5.40 +
5.41 +text{*
5.42 +The following example was taken from HOL/ex/PresburgerEx.thy, where it says:
5.43 +
5.44 + This following theorem proves that all solutions to the
5.45 + recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with
5.46 + period 9. The example was brought to our attention by John
5.47 + Harrison. It does does not require Presburger arithmetic but merely
5.48 + quantifier-free linear arithmetic and holds for the rationals as well.
5.49 +
5.50 + Warning: it takes (in 2006) over 4.2 minutes!
5.51 +
5.52 +There, it is proved by "arith". SMT is able to prove this within a fraction
5.53 +of one second.
5.54 +*}
5.55 +
5.56 +lemma "\<lbrakk> x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3;
5.57 + x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6;
5.58 + x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \<rbrakk>
5.59 + \<Longrightarrow> x1 = x10 & x2 = (x11::int)"
5.60 + by smt
5.61 +
5.62 +lemma "\<exists>x::int. 0 < x" by smt
5.63 +lemma "\<exists>x::real. 0 < x" by smt
5.64 +lemma "\<forall>x y::int. x < y \<longrightarrow> (2 * x + 1) < (2 * y)" by smt
5.65 +lemma "\<forall>x y::int. (2 * x + 1) \<noteq> (2 * y)" by smt
5.66 +lemma "~ (\<exists>x y z::int. 4 * x + -6 * y = (1::int))" by smt
5.67 +lemma "~ (\<exists>x::int. False)" by smt
5.68 +
5.69 +
5.70 +section {* Non-linear arithmetic *}
5.71 +
5.72 +lemma "((x::int) * (1 + y) - x * (1 - y)) = (2 * x * y)" by smt
5.73 +lemma
5.74 + "(U::int) + (1 + p) * (b + e) + p * d =
5.75 + U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
5.76 + by smt
5.77 +
5.78 +
5.79 +section {* Linear arithmetic for natural numbers *}
5.80 +
5.81 +lemma "a < 3 \<Longrightarrow> (7::nat) > 2 * a" by smt
5.82 +lemma "let x = (1::nat) + y in x - y > 0 * x" by smt
5.83 +lemma
5.84 + "let x = (1::nat) + y in
5.85 + let P = (if x > 0 then True else False) in
5.86 + False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
5.87 + by smt
5.88 +
5.89 +
5.90 +section {* Bitvectors *}
5.91 +
5.92 +locale bv
5.93 +begin
5.94 +
5.95 +declare [[smt_solver=z3]]
5.96 +
5.97 +lemma "(27 :: 4 word) = -5" by smt
5.98 +lemma "(27 :: 4 word) = 11" by smt
5.99 +lemma "23 < (27::8 word)" by smt
5.100 +lemma "27 + 11 = (6::5 word)" by smt
5.101 +lemma "7 * 3 = (21::8 word)" by smt
5.102 +lemma "11 - 27 = (-16::8 word)" by smt
5.103 +lemma "- -11 = (11::5 word)" by smt
5.104 +lemma "-40 + 1 = (-39::7 word)" by smt
5.105 +lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by smt
5.106 +
5.107 +lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by smt
5.108 +lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by smt
5.109 +lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by smt
5.110 +lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by smt
5.111 +
5.112 +lemma "word_cat (27::4 word) (27::8 word) = (2843::12 word)" by smt
5.113 +lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
5.114 + by smt
5.115 +
5.116 +lemma "slice 1 (0b10110 :: 4 word) = (0b11 :: 2 word)" by smt
5.117 +
5.118 +lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by smt
5.119 +lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by smt
5.120 +
5.121 +lemma "bv_lshr 0b10011 2 = (0b100::8 word)" by smt
5.122 +lemma "bv_ashr 0b10011 2 = (0b100::8 word)" by smt
5.123 +
5.124 +lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by smt
5.125 +lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by smt
5.126 +
5.127 +lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by smt
5.128 +
5.129 +lemma "w < 256 \<Longrightarrow> (w :: 16 word) AND 0x00FF = w" by smt
5.130 +
5.131 +end
5.132 +
5.133 +
5.134 +section {* Pairs *}
5.135 +
5.136 +lemma "fst (x, y) = a \<Longrightarrow> x = a" by smt
5.137 +lemma "p1 = (x, y) \<and> p2 = (y, x) \<Longrightarrow> fst p1 = snd p2" by smt
5.138 +
5.139 +
5.140 +section {* Higher-order problems and recursion *}
5.141 +
5.142 +lemma "(f g x = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)" by smt
5.143 +lemma "P ((2::int) < 3) = P True" by smt
5.144 +lemma "P ((2::int) < 3) = (P True :: bool)" by smt
5.145 +lemma "P (0 \<le> (a :: 4 word)) = P True" using [[smt_solver=z3]] by smt
5.146 +lemma "id 3 = 3 \<and> id True = True" by (smt add: id_def)
5.147 +lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i" by smt
5.148 +lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt add: map.simps)
5.149 +lemma "(ALL x. P x) | ~ All P" by smt
5.150 +
5.151 +fun dec_10 :: "nat \<Rightarrow> nat" where
5.152 + "dec_10 n = (if n < 10 then n else dec_10 (n - 10))"
5.153 +lemma "dec_10 (4 * dec_10 4) = 6" by (smt add: dec_10.simps)
5.154 +
5.155 +axiomatization
5.156 + eval_dioph :: "int list \<Rightarrow> nat list \<Rightarrow> int"
5.157 + where
5.158 + eval_dioph_mod:
5.159 + "eval_dioph ks xs mod int n = eval_dioph ks (map (\<lambda>x. x mod n) xs) mod int n"
5.160 + and
5.161 + eval_dioph_div_mult:
5.162 + "eval_dioph ks (map (\<lambda>x. x div n) xs) * int n +
5.163 + eval_dioph ks (map (\<lambda>x. x mod n) xs) = eval_dioph ks xs"
5.164 +lemma
5.165 + "(eval_dioph ks xs = l) =
5.166 + (eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and>
5.167 + eval_dioph ks (map (\<lambda>x. x div 2) xs) =
5.168 + (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
5.169 + by (smt add: eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
5.170 +
5.171 +
5.172 +section {* Monomorphization examples *}
5.173 +
5.174 +definition P :: "'a \<Rightarrow> bool" where "P x = True"
5.175 +lemma poly_P: "P x \<and> (P [x] \<or> \<not>P[x])" by (simp add: P_def)
5.176 +lemma "P (1::int)" by (smt add: poly_P)
5.177 +
5.178 +consts g :: "'a \<Rightarrow> nat"
5.179 +axioms
5.180 + g1: "g (Some x) = g [x]"
5.181 + g2: "g None = g []"
5.182 + g3: "g xs = length xs"
5.183 +lemma "g (Some (3::int)) = g (Some True)" by (smt add: g1 g2 g3 list.size)
5.184 +
5.185 +end
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/SMT/IsaMakefile Fri Sep 18 18:13:19 2009 +0200
6.3 @@ -0,0 +1,39 @@
6.4 +
6.5 +## targets
6.6 +
6.7 +default: HOL-SMT
6.8 +images: HOL-SMT
6.9 +test:
6.10 +
6.11 +all: images test
6.12 +
6.13 +
6.14 +## global settings
6.15 +
6.16 +SRC = $(ISABELLE_HOME)/src
6.17 +OUT = $(ISABELLE_OUTPUT)
6.18 +LOG = $(OUT)/log
6.19 +
6.20 +USEDIR = $(ISATOOL) usedir -v true
6.21 +
6.22 +
6.23 +## HOL-SMT
6.24 +
6.25 +HOL-SMT: $(OUT)/HOL-SMT
6.26 +
6.27 +$(OUT)/HOL-SMT: $(OUT)/HOL-Word ROOT.ML SMT_Definitions.thy SMT.thy \
6.28 + Tools/cancel_conj_disj.ML Tools/smt_normalize.ML Tools/smt_monomorph.ML \
6.29 + Tools/smt_translate.ML Tools/smt_builtin.ML Tools/smtlib_interface.ML \
6.30 + Tools/smt_solver.ML Tools/cvc3_solver.ML Tools/yices_solver.ML \
6.31 + Tools/z3_interface.ML Tools/z3_solver.ML Tools/z3_model.ML \
6.32 + Tools/z3_proof.ML Tools/z3_proof_rules.ML Tools/z3_proof_terms.ML
6.33 + @$(USEDIR) -b HOL-Word HOL-SMT
6.34 +
6.35 +$(OUT)/HOL-Word:
6.36 + @$(ISATOOL) make HOL-Word -C $(SRC)/HOL
6.37 +
6.38 +
6.39 +## clean
6.40 +
6.41 +clean:
6.42 + @rm -f $(OUT)/HOL-SMT
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/SMT/ROOT.ML Fri Sep 18 18:13:19 2009 +0200
7.3 @@ -0,0 +1,1 @@
7.4 +use_thy "SMT";
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/SMT/SMT.thy Fri Sep 18 18:13:19 2009 +0200
8.3 @@ -0,0 +1,51 @@
8.4 +(* Title: HOL/SMT/SMT.thy
8.5 + Author: Sascha Boehme, TU Muenchen
8.6 +*)
8.7 +
8.8 +header {* SMT method using external SMT solvers (CVC3, Yices, Z3) *}
8.9 +
8.10 +theory SMT
8.11 +imports SMT_Definitions
8.12 +uses
8.13 + "Tools/smt_normalize.ML"
8.14 + "Tools/smt_monomorph.ML"
8.15 + "Tools/smt_translate.ML"
8.16 + "Tools/smt_solver.ML"
8.17 + "Tools/smtlib_interface.ML"
8.18 + "Tools/cvc3_solver.ML"
8.19 + "Tools/yices_solver.ML"
8.20 + "Tools/z3_model.ML"
8.21 + "Tools/z3_interface.ML"
8.22 + "Tools/z3_solver.ML"
8.23 +begin
8.24 +
8.25 +setup {*
8.26 + SMT_Normalize.setup #>
8.27 + SMT_Solver.setup #>
8.28 + CVC3_Solver.setup #>
8.29 + Yices_Solver.setup #>
8.30 + Z3_Solver.setup
8.31 +*}
8.32 +
8.33 +ML {*
8.34 +OuterSyntax.improper_command "smt_status"
8.35 + "Show the available SMT solvers and the currently selected solver."
8.36 + OuterKeyword.diag
8.37 + (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
8.38 + SMT_Solver.print_setup (Context.Proof (Toplevel.context_of state)))))
8.39 +*}
8.40 +
8.41 +method_setup smt = {*
8.42 + let fun solver thms ctxt = SMT_Solver.smt_tac ctxt thms
8.43 + in
8.44 + Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [] >>
8.45 + (Method.SIMPLE_METHOD' oo solver)
8.46 + end
8.47 +*} "Applies an SMT solver to the current goal."
8.48 +
8.49 +declare [[ smt_solver = z3, smt_timeout = 20, smt_trace = false ]]
8.50 +declare [[ smt_unfold_defs = true ]]
8.51 +declare [[ z3_proofs = false ]]
8.52 +
8.53 +end
8.54 +
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/SMT/SMT_Definitions.thy Fri Sep 18 18:13:19 2009 +0200
9.3 @@ -0,0 +1,113 @@
9.4 +(* Title: HOL/SMT/SMT_Definitions.thy
9.5 + Author: Sascha Boehme, TU Muenchen
9.6 +*)
9.7 +
9.8 +header {* SMT-specific definitions *}
9.9 +
9.10 +theory SMT_Definitions
9.11 +imports Real Word "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
9.12 +begin
9.13 +
9.14 +section {* Triggers for quantifier instantiation *}
9.15 +
9.16 +text {*
9.17 +Some SMT solvers support triggers for quantifier instantiation. Each trigger
9.18 +consists of one ore more patterns. A pattern may either be a list of positive
9.19 +subterms (the first being tagged by "pat" and the consecutive subterms tagged
9.20 +by "andpat"), or a list of negative subterms (the first being tagged by "nopat"
9.21 +and the consecutive subterms tagged by "andpat").
9.22 +*}
9.23 +
9.24 +datatype pattern = Pattern
9.25 +
9.26 +definition pat :: "'a \<Rightarrow> pattern"
9.27 +where "pat _ = Pattern"
9.28 +
9.29 +definition nopat :: "bool \<Rightarrow> pattern"
9.30 +where "nopat _ = Pattern"
9.31 +
9.32 +definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)
9.33 +where "_ andpat _ = Pattern"
9.34 +
9.35 +definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool"
9.36 +where "trigger _ P = P"
9.37 +
9.38 +
9.39 +section {* Arithmetic *}
9.40 +
9.41 +text {*
9.42 +The sign of @{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"} follows the sign of the
9.43 +divisor. In contrast to that, the sign of the following operation is that of
9.44 +the dividend.
9.45 +*}
9.46 +
9.47 +definition rem :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "rem" 70)
9.48 +where "a rem b =
9.49 + (if (a \<ge> 0 \<and> b < 0) \<or> (a < 0 \<and> b \<ge> 0) then - (a mod b) else a mod b)"
9.50 +
9.51 +text {* A decision procedure for linear real arithmetic: *}
9.52 +
9.53 +setup {*
9.54 + Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac)
9.55 +*}
9.56 +
9.57 +
9.58 +section {* Bitvectors *}
9.59 +
9.60 +text {*
9.61 +The following definitions provide additional functions not found in HOL-Word.
9.62 +*}
9.63 +
9.64 +definition sdiv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "sdiv" 70)
9.65 +where "w1 sdiv w2 = word_of_int (sint w1 div sint w2)"
9.66 +
9.67 +definition smod :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "smod" 70)
9.68 + (* sign follows divisor *)
9.69 +where "w1 smod w2 = word_of_int (sint w1 mod sint w2)"
9.70 +
9.71 +definition srem :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "srem" 70)
9.72 + (* sign follows dividend *)
9.73 +where "w1 srem w2 = word_of_int (sint w1 rem sint w2)"
9.74 +
9.75 +definition bv_shl :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
9.76 +where "bv_shl w1 w2 = (w1 << unat w2)"
9.77 +
9.78 +definition bv_lshr :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
9.79 +where "bv_lshr w1 w2 = (w1 >> unat w2)"
9.80 +
9.81 +definition bv_ashr :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word"
9.82 +where "bv_ashr w1 w2 = (w1 >>> unat w2)"
9.83 +
9.84 +
9.85 +section {* Higher-order encoding *}
9.86 +
9.87 +definition "apply" where "apply f x = f x"
9.88 +
9.89 +
9.90 +section {* First-order logic *}
9.91 +
9.92 +text {*
9.93 +Some SMT solver formats require a strict separation between formulas and terms.
9.94 +The following marker symbols are used internally to separate those categories:
9.95 +*}
9.96 +
9.97 +definition formula :: "bool \<Rightarrow> bool" where "formula x = x"
9.98 +definition "term" where "term x = x"
9.99 +
9.100 +text {*
9.101 +Predicate symbols also occurring as function symbols are turned into function
9.102 +symbols by translating atomic formulas into terms:
9.103 +*}
9.104 +
9.105 +abbreviation holds :: "bool \<Rightarrow> bool" where "holds \<equiv> (\<lambda>P. term P = term True)"
9.106 +
9.107 +text {*
9.108 +The following constant represents equivalence, to be treated differently than
9.109 +the (polymorphic) equality predicate:
9.110 +*}
9.111 +
9.112 +definition iff :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "iff" 50) where
9.113 + "(x iff y) = (x = y)"
9.114 +
9.115 +end
9.116 +
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/HOL/SMT/Tools/cvc3_solver.ML Fri Sep 18 18:13:19 2009 +0200
10.3 @@ -0,0 +1,59 @@
10.4 +(* Title: HOL/SMT/Tools/cvc3_solver.ML
10.5 + Author: Sascha Boehme, TU Muenchen
10.6 +
10.7 +Interface of the SMT solver CVC3.
10.8 +*)
10.9 +
10.10 +signature CVC3_SOLVER =
10.11 +sig
10.12 + val setup: theory -> theory
10.13 +end
10.14 +
10.15 +structure CVC3_Solver: CVC3_SOLVER =
10.16 +struct
10.17 +
10.18 +val solver_name = "cvc3"
10.19 +val env_var = "CVC3_SOLVER"
10.20 +
10.21 +val options =
10.22 + ["+counterexample", "-lang", "smtlib", "-output-lang", "presentation"]
10.23 +
10.24 +val is_sat = String.isPrefix "Satisfiable."
10.25 +val is_unsat = String.isPrefix "Unsatisfiable."
10.26 +val is_unknown = String.isPrefix "Unknown."
10.27 +
10.28 +fun cex_kind true = "Counterexample"
10.29 + | cex_kind false = "Possible counterexample"
10.30 +
10.31 +fun raise_cex real ctxt recon ls =
10.32 + let
10.33 + val start = String.isPrefix "%Satisfiable Variable Assignment: %"
10.34 + val index = find_index start ls
10.35 + val ls = if index > 0 then Library.drop (index + 1, ls) else []
10.36 + val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls)
10.37 + in error (Pretty.string_of p) end
10.38 +
10.39 +fun core_oracle (SMT_Solver.ProofData {context, output, recon, ...}) =
10.40 + let
10.41 + val empty_line = (fn "" => true | _ => false)
10.42 + val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
10.43 + val (l, ls) = split_first (dropwhile empty_line output)
10.44 + in
10.45 + if is_unsat l then @{cprop False}
10.46 + else if is_sat l then raise_cex true context recon ls
10.47 + else if is_unknown l then raise_cex false context recon ls
10.48 + else error (solver_name ^ " failed")
10.49 + end
10.50 +
10.51 +fun smtlib_solver oracle _ =
10.52 + SMT_Solver.SolverConfig {
10.53 + name = {env_var=env_var, remote_name=solver_name},
10.54 + interface = SMTLIB_Interface.interface,
10.55 + arguments = options,
10.56 + reconstruct = oracle }
10.57 +
10.58 +val setup =
10.59 + Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
10.60 + SMT_Solver.add_solver (solver_name, smtlib_solver oracle))
10.61 +
10.62 +end
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/HOL/SMT/Tools/smt_builtin.ML Fri Sep 18 18:13:19 2009 +0200
11.3 @@ -0,0 +1,78 @@
11.4 +(* Title: HOL/SMT/Tools/smt_builtin.ML
11.5 + Author: Sascha Boehme, TU Muenchen
11.6 +
11.7 +Tables for built-in symbols.
11.8 +*)
11.9 +
11.10 +signature SMT_BUILTIN =
11.11 +sig
11.12 + type sterm = (SMT_Translate.sym, typ) sterm
11.13 + type builtin_fun = typ -> sterm list -> (string * sterm list) option
11.14 + type table = (typ * builtin_fun) list Symtab.table
11.15 +
11.16 + val make: (term * string) list -> table
11.17 + val add: term * builtin_fun -> table -> table
11.18 + val lookup: table -> theory -> string * typ -> sterm list ->
11.19 + (string * sterm list) option
11.20 +
11.21 + val bv_rotate: (int -> string) -> builtin_fun
11.22 + val bv_extend: (int -> string) -> builtin_fun
11.23 + val bv_extract: (int -> int -> string) -> builtin_fun
11.24 +end
11.25 +
11.26 +structure SMT_Builtin: SMT_BUILTIN =
11.27 +struct
11.28 +
11.29 +structure T = SMT_Translate
11.30 +
11.31 +type sterm = (SMT_Translate.sym, typ) sterm
11.32 +type builtin_fun = typ -> sterm list -> (string * sterm list) option
11.33 +type table = (typ * builtin_fun) list Symtab.table
11.34 +
11.35 +fun make entries =
11.36 + let
11.37 + fun dest (t, bn) =
11.38 + let val (n, T) = Term.dest_Const t
11.39 + in (n, (Logic.varifyT T, K (pair bn))) end
11.40 + in Symtab.make (AList.group (op =) (map dest entries)) end
11.41 +
11.42 +fun add (t, f) tab =
11.43 + let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t)
11.44 + in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end
11.45 +
11.46 +fun lookup tab thy (n, T) =
11.47 + AList.lookup (Sign.typ_instance thy) (Symtab.lookup_list tab n) T T
11.48 +
11.49 +
11.50 +fun dest_binT T =
11.51 + (case T of
11.52 + Type (@{type_name "Numeral_Type.num0"}, _) => 0
11.53 + | Type (@{type_name "Numeral_Type.num1"}, _) => 1
11.54 + | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
11.55 + | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
11.56 + | _ => raise TYPE ("dest_binT", [T], []))
11.57 +
11.58 +fun dest_wordT T =
11.59 + (case T of
11.60 + Type (@{type_name "word"}, [T]) => dest_binT T
11.61 + | _ => raise TYPE ("dest_wordT", [T], []))
11.62 +
11.63 +
11.64 +val dest_nat = (fn
11.65 + SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i
11.66 + | _ => NONE)
11.67 +
11.68 +fun bv_rotate mk_name T ts =
11.69 + dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts))
11.70 +
11.71 +fun bv_extend mk_name T ts =
11.72 + (case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of
11.73 + (SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE
11.74 + | _ => NONE)
11.75 +
11.76 +fun bv_extract mk_name T ts =
11.77 + (case (try dest_wordT (body_type T), dest_nat (hd ts)) of
11.78 + (SOME i, SOME lb) => SOME (mk_name (i + lb - 1) lb, tl ts)
11.79 + | _ => NONE)
11.80 +
11.81 +end
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/HOL/SMT/Tools/smt_monomorph.ML Fri Sep 18 18:13:19 2009 +0200
12.3 @@ -0,0 +1,120 @@
12.4 +(* Title: HOL/SMT/Tools/smt_monomorph.ML
12.5 + Author: Sascha Boehme, TU Muenchen
12.6 +
12.7 +Monomorphization of terms, i.e., computation of all (necessary) instances.
12.8 +*)
12.9 +
12.10 +signature SMT_MONOMORPH =
12.11 +sig
12.12 + val monomorph: theory -> term list -> term list
12.13 +end
12.14 +
12.15 +structure SMT_Monomorph: SMT_MONOMORPH =
12.16 +struct
12.17 +
12.18 +fun selection [] = []
12.19 + | selection (x :: xs) = (x, xs) :: map (apsnd (cons x)) (selection xs)
12.20 +
12.21 +fun permute [] = []
12.22 + | permute [x] = [[x]]
12.23 + | permute xs = maps (fn (y, ys) => map (cons y) (permute ys)) (selection xs)
12.24 +
12.25 +fun fold_all f = fold (fn x => maps (f x))
12.26 +
12.27 +
12.28 +val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
12.29 +val term_has_tvars = Term.exists_type typ_has_tvars
12.30 +
12.31 +val ignored = member (op =) [
12.32 + @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
12.33 + @{const_name "op ="}, @{const_name zero_class.zero},
12.34 + @{const_name one_class.one}, @{const_name number_of}]
12.35 +fun consts_of ts = AList.group (op =) (fold Term.add_consts ts [])
12.36 + |> filter_out (ignored o fst)
12.37 +
12.38 +val join_consts = curry (AList.join (op =) (K (merge (op =))))
12.39 +fun diff_consts cs ds =
12.40 + let fun diff (n, Ts) =
12.41 + (case AList.lookup (op =) cs n of
12.42 + NONE => SOME (n, Ts)
12.43 + | SOME Us =>
12.44 + let val Ts' = fold (remove (op =)) Us Ts
12.45 + in if null Ts' then NONE else SOME (n, Ts') end)
12.46 + in map_filter diff ds end
12.47 +
12.48 +fun instances thy is (n, Ts) env =
12.49 + let
12.50 + val Us = these (AList.lookup (op =) is n)
12.51 + val Ts' = filter typ_has_tvars (map (Envir.subst_type env) Ts)
12.52 + in
12.53 + (case map_product pair Ts' Us of
12.54 + [] => [env]
12.55 + | TUs => map_filter (try (fn TU => Sign.typ_match thy TU env)) TUs)
12.56 + end
12.57 +
12.58 +fun proper_match ps env =
12.59 + forall (forall (not o typ_has_tvars o Envir.subst_type env) o snd) ps
12.60 +
12.61 +val eq_tab = gen_eq_set (op =) o pairself Vartab.dest
12.62 +
12.63 +fun specialize thy cs is ((r, ps), ces) (ts, ns) =
12.64 + let
12.65 + val ps' = filter (AList.defined (op =) is o fst) ps
12.66 +
12.67 + val envs = permute ps'
12.68 + |> maps (fn ps => fold_all (instances thy is) ps [Vartab.empty])
12.69 + |> filter (proper_match ps')
12.70 + |> filter_out (member eq_tab ces)
12.71 + |> distinct eq_tab
12.72 +
12.73 + val us = map (fn env => Envir.subst_term_types env r) envs
12.74 + val ns' = join_consts (diff_consts is (diff_consts cs (consts_of us))) ns
12.75 + in (envs @ ces, (fold (insert (op aconv)) us ts, ns')) end
12.76 +
12.77 +
12.78 +fun incr_tvar_indices i t =
12.79 + let
12.80 + val incrT = Logic.incr_tvar i
12.81 +
12.82 + fun incr t =
12.83 + (case t of
12.84 + Const (n, T) => Const (n, incrT T)
12.85 + | Free (n, T) => Free (n, incrT T)
12.86 + | Abs (n, T, t1) => Abs (n, incrT T, incr t1)
12.87 + | t1 $ t2 => incr t1 $ incr t2
12.88 + | _ => t)
12.89 + in incr t end
12.90 +
12.91 +
12.92 +val monomorph_limit = 10
12.93 +
12.94 +(* Instantiate all polymorphic constants (i.e., constants occurring both with
12.95 + ground types and type variables) with all (necessary) ground types; thereby
12.96 + create copies of terms containing those constants.
12.97 + To prevent non-termination, there is an upper limit for the number of
12.98 + recursions involved in the fixpoint construction. *)
12.99 +fun monomorph thy ts =
12.100 + let
12.101 + val (ps, ms) = List.partition term_has_tvars ts
12.102 +
12.103 + fun with_tvar (n, Ts) =
12.104 + let val Ts' = filter typ_has_tvars Ts
12.105 + in if null Ts' then NONE else SOME (n, Ts') end
12.106 + fun incr t idx = (incr_tvar_indices idx t, idx + Term.maxidx_of_term t + 1)
12.107 + val rps = fst (fold_map incr ps 0)
12.108 + |> map (fn r => (r, map_filter with_tvar (consts_of [r])))
12.109 +
12.110 + fun mono count is ces cs ts =
12.111 + let
12.112 + val spec = specialize thy cs is
12.113 + val (ces', (ts', is')) = fold_map spec (rps ~~ ces) (ts, [])
12.114 + val cs' = join_consts is cs
12.115 + in
12.116 + if null is' then ts'
12.117 + else if count > monomorph_limit then
12.118 + (Output.warning "monomorphization limit reached"; ts')
12.119 + else mono (count + 1) is' ces' cs' ts'
12.120 + end
12.121 + in mono 0 (consts_of ms) (map (K []) rps) [] ms end
12.122 +
12.123 +end
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/HOL/SMT/Tools/smt_normalize.ML Fri Sep 18 18:13:19 2009 +0200
13.3 @@ -0,0 +1,408 @@
13.4 +(* Title: HOL/SMT/Tools/smt_normalize.ML
13.5 + Author: Sascha Boehme, TU Muenchen
13.6 +
13.7 +Normalization steps on theorems required by SMT solvers:
13.8 + * unfold trivial let expressions,
13.9 + * replace negative numerals by negated positive numerals,
13.10 + * embed natural numbers into integers,
13.11 + * add extra rules specifying types and constants which occur frequently,
13.12 + * lift lambda terms,
13.13 + * make applications explicit for functions with varying number of arguments,
13.14 + * fully translate into object logic, add universal closure.
13.15 +*)
13.16 +
13.17 +signature SMT_NORMALIZE =
13.18 +sig
13.19 + val normalize_rule: Proof.context -> thm -> thm
13.20 + val instantiate_free: Thm.cterm * Thm.cterm -> thm -> thm
13.21 + val discharge_definition: Thm.cterm -> thm -> thm
13.22 +
13.23 + val trivial_let: Proof.context -> thm list -> thm list
13.24 + val positive_numerals: Proof.context -> thm list -> thm list
13.25 + val nat_as_int: Proof.context -> thm list -> thm list
13.26 + val unfold_defs: bool Config.T
13.27 + val add_pair_rules: Proof.context -> thm list -> thm list
13.28 + val add_fun_upd_rules: Proof.context -> thm list -> thm list
13.29 + val add_abs_min_max_rules: Proof.context -> thm list -> thm list
13.30 +
13.31 + datatype config =
13.32 + RewriteTrivialLets |
13.33 + RewriteNegativeNumerals |
13.34 + RewriteNaturalNumbers |
13.35 + AddPairRules |
13.36 + AddFunUpdRules |
13.37 + AddAbsMinMaxRules
13.38 +
13.39 + val normalize: config list -> Proof.context -> thm list ->
13.40 + Thm.cterm list * thm list
13.41 +
13.42 + val setup: theory -> theory
13.43 +end
13.44 +
13.45 +structure SMT_Normalize: SMT_NORMALIZE =
13.46 +struct
13.47 +
13.48 +val norm_binder_conv = Conv.try_conv (More_Conv.rewrs_conv [
13.49 + @{lemma "All P == ALL x. P x" by (rule reflexive)},
13.50 + @{lemma "Ex P == EX x. P x" by (rule reflexive)},
13.51 + @{lemma "Let c P == let x = c in P x" by (rule reflexive)}])
13.52 +
13.53 +fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
13.54 +
13.55 +fun norm_meta_def cv thm =
13.56 + let val thm' = Thm.combination thm (Thm.reflexive cv)
13.57 + in Thm.transitive thm' (Thm.beta_conversion false (Thm.rhs_of thm')) end
13.58 +
13.59 +fun norm_def ctxt thm =
13.60 + (case Thm.prop_of thm of
13.61 + Const (@{const_name "=="}, _) $ _ $ Abs (_, T, _) =>
13.62 + let val v = Var ((Name.uu, #maxidx (Thm.rep_thm thm) + 1), T)
13.63 + in norm_def ctxt (norm_meta_def (cert ctxt v) thm) end
13.64 + | @{term Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ Abs _) =>
13.65 + norm_def ctxt (thm RS @{thm fun_cong})
13.66 + | _ => thm)
13.67 +
13.68 +fun normalize_rule ctxt =
13.69 + Conv.fconv_rule (
13.70 + Thm.beta_conversion true then_conv
13.71 + Thm.eta_conversion then_conv
13.72 + More_Conv.bottom_conv (K norm_binder_conv) ctxt) #>
13.73 + norm_def ctxt #>
13.74 + Drule.forall_intr_vars #>
13.75 + Conv.fconv_rule ObjectLogic.atomize
13.76 +
13.77 +fun instantiate_free (cv, ct) thm =
13.78 + if Term.exists_subterm (equal (Thm.term_of cv)) (Thm.prop_of thm)
13.79 + then Thm.forall_elim ct (Thm.forall_intr cv thm)
13.80 + else thm
13.81 +
13.82 +fun discharge_definition ct thm =
13.83 + let val (cv, cu) = Thm.dest_equals ct
13.84 + in
13.85 + Thm.implies_intr ct thm
13.86 + |> instantiate_free (cv, cu)
13.87 + |> (fn thm => Thm.implies_elim thm (Thm.reflexive cu))
13.88 + end
13.89 +
13.90 +fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct
13.91 +fun if_true_conv c cv = if_conv c cv Conv.all_conv
13.92 +
13.93 +
13.94 +(* simplification of trivial let expressions (whose bound variables occur at
13.95 + most once) *)
13.96 +
13.97 +local
13.98 + fun count i (Bound j) = if j = i then 1 else 0
13.99 + | count i (t $ u) = count i t + count i u
13.100 + | count i (Abs (_, _, t)) = count (i + 1) t
13.101 + | count _ _ = 0
13.102 +
13.103 + fun is_trivial_let (Const (@{const_name Let}, _) $ _ $ Abs (_, _, t)) =
13.104 + (count 0 t <= 1)
13.105 + | is_trivial_let _ = false
13.106 +
13.107 + fun let_conv _ = if_true_conv is_trivial_let (Conv.rewr_conv @{thm Let_def})
13.108 +
13.109 + fun cond_let_conv ctxt = if_true_conv (Term.exists_subterm is_trivial_let)
13.110 + (More_Conv.top_conv let_conv ctxt)
13.111 +in
13.112 +fun trivial_let ctxt = map (Conv.fconv_rule (cond_let_conv ctxt))
13.113 +end
13.114 +
13.115 +
13.116 +(* rewriting of negative integer numerals into positive numerals *)
13.117 +
13.118 +local
13.119 + fun neg_numeral @{term Int.Min} = true
13.120 + | neg_numeral _ = false
13.121 + fun is_number_sort thy T = Sign.of_sort thy (T, @{sort number_ring})
13.122 + fun is_neg_number ctxt (Const (@{const_name number_of}, T) $ t) =
13.123 + Term.exists_subterm neg_numeral t andalso
13.124 + is_number_sort (ProofContext.theory_of ctxt) (Term.body_type T)
13.125 + | is_neg_number _ _ = false
13.126 + fun has_neg_number ctxt = Term.exists_subterm (is_neg_number ctxt)
13.127 +
13.128 + val pos_numeral_ss = HOL_ss
13.129 + addsimps [@{thm Int.number_of_minus}, @{thm Int.number_of_Min}]
13.130 + addsimps [@{thm Int.numeral_1_eq_1}]
13.131 + addsimps @{thms Int.pred_bin_simps}
13.132 + addsimps @{thms Int.normalize_bin_simps}
13.133 + addsimps @{lemma
13.134 + "Int.Min = - Int.Bit1 Int.Pls"
13.135 + "Int.Bit0 (- Int.Pls) = - Int.Pls"
13.136 + "Int.Bit0 (- k) = - Int.Bit0 k"
13.137 + "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
13.138 + by simp_all (simp add: pred_def)}
13.139 +
13.140 + fun pos_conv ctxt = if_conv (is_neg_number ctxt)
13.141 + (Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss))
13.142 + Conv.no_conv
13.143 +
13.144 + fun cond_pos_conv ctxt = if_true_conv (has_neg_number ctxt)
13.145 + (More_Conv.top_sweep_conv pos_conv ctxt)
13.146 +in
13.147 +fun positive_numerals ctxt = map (Conv.fconv_rule (cond_pos_conv ctxt))
13.148 +end
13.149 +
13.150 +
13.151 +(* embedding of standard natural number operations into integer operations *)
13.152 +
13.153 +local
13.154 + val nat_embedding = @{lemma
13.155 + "nat (int n) = n"
13.156 + "i >= 0 --> int (nat i) = i"
13.157 + "i < 0 --> int (nat i) = 0"
13.158 + by simp_all}
13.159 +
13.160 + val nat_rewriting = @{lemma
13.161 + "0 = nat 0"
13.162 + "1 = nat 1"
13.163 + "number_of i = nat (number_of i)"
13.164 + "int (nat 0) = 0"
13.165 + "int (nat 1) = 1"
13.166 + "a < b = (int a < int b)"
13.167 + "a <= b = (int a <= int b)"
13.168 + "Suc a = nat (int a + 1)"
13.169 + "a + b = nat (int a + int b)"
13.170 + "a - b = nat (int a - int b)"
13.171 + "a * b = nat (int a * int b)"
13.172 + "a div b = nat (int a div int b)"
13.173 + "a mod b = nat (int a mod int b)"
13.174 + "int (nat (int a + int b)) = int a + int b"
13.175 + "int (nat (int a * int b)) = int a * int b"
13.176 + "int (nat (int a div int b)) = int a div int b"
13.177 + "int (nat (int a mod int b)) = int a mod int b"
13.178 + by (simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib
13.179 + int_mult[symmetric] zdiv_int[symmetric] zmod_int[symmetric])+}
13.180 +
13.181 + fun on_positive num f x =
13.182 + (case try HOLogic.dest_number (Thm.term_of num) of
13.183 + SOME (_, i) => if i >= 0 then SOME (f x) else NONE
13.184 + | NONE => NONE)
13.185 +
13.186 + val cancel_int_nat_ss = HOL_ss
13.187 + addsimps [@{thm Nat_Numeral.nat_number_of}]
13.188 + addsimps [@{thm Nat_Numeral.int_nat_number_of}]
13.189 + addsimps @{thms neg_simps}
13.190 +
13.191 + fun cancel_int_nat_simproc _ ss ct =
13.192 + let
13.193 + val num = Thm.dest_arg (Thm.dest_arg ct)
13.194 + val goal = Thm.mk_binop @{cterm "op == :: int => _"} ct num
13.195 + val simpset = Simplifier.inherit_context ss cancel_int_nat_ss
13.196 + fun tac _ = Simplifier.simp_tac simpset 1
13.197 + in on_positive num (Goal.prove_internal [] goal) tac end
13.198 +
13.199 + val nat_ss = HOL_ss
13.200 + addsimps nat_rewriting
13.201 + addsimprocs [Simplifier.make_simproc {
13.202 + name = "cancel_int_nat_num", lhss = [@{cpat "int (nat _)"}],
13.203 + proc = cancel_int_nat_simproc, identifier = [] }]
13.204 +
13.205 + fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss)
13.206 +
13.207 + val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
13.208 +in
13.209 +fun nat_as_int ctxt thms =
13.210 + let
13.211 + fun norm thm uses_nat =
13.212 + if not (uses_nat_type (Thm.prop_of thm)) then (thm, uses_nat)
13.213 + else (Conv.fconv_rule (conv ctxt) thm, true)
13.214 + val (thms', uses_nat) = fold_map norm thms false
13.215 + in if uses_nat then nat_embedding @ thms' else thms' end
13.216 +end
13.217 +
13.218 +
13.219 +(* include additional rules *)
13.220 +
13.221 +val (unfold_defs, unfold_defs_setup) =
13.222 + Attrib.config_bool "smt_unfold_defs" true
13.223 +
13.224 +local
13.225 + val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
13.226 +
13.227 + val pair_type = (fn Type (@{type_name "*"}, _) => true | _ => false)
13.228 + val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
13.229 +
13.230 + val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
13.231 + val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
13.232 + val exists_fun_upd = Term.exists_subterm is_fun_upd
13.233 +in
13.234 +fun add_pair_rules _ thms =
13.235 + thms
13.236 + |> exists (exists_pair_type o Thm.prop_of) thms ? append pair_rules
13.237 +
13.238 +fun add_fun_upd_rules _ thms =
13.239 + thms
13.240 + |> exists (exists_fun_upd o Thm.prop_of) thms ? append fun_upd_rules
13.241 +end
13.242 +
13.243 +
13.244 +local
13.245 + fun mk_entry t thm = (Term.head_of t, (thm, thm RS @{thm eq_reflection}))
13.246 + fun prepare_def thm =
13.247 + (case HOLogic.dest_Trueprop (Thm.prop_of thm) of
13.248 + Const (@{const_name "op ="}, _) $ t $ _ => mk_entry t thm
13.249 + | t => raise TERM ("prepare_def", [t]))
13.250 +
13.251 + val defs = map prepare_def [
13.252 + @{thm abs_if[where 'a = int]}, @{thm abs_if[where 'a = real]},
13.253 + @{thm min_def[where 'a = int]}, @{thm min_def[where 'a = real]},
13.254 + @{thm max_def[where 'a = int]}, @{thm max_def[where 'a = real]}]
13.255 +
13.256 + fun add_sym t = if AList.defined (op =) defs t then insert (op =) t else I
13.257 + fun add_syms thms = fold (Term.fold_aterms add_sym o Thm.prop_of) thms []
13.258 +
13.259 + fun unfold_conv ctxt ct =
13.260 + (case AList.lookup (op =) defs (Term.head_of (Thm.term_of ct)) of
13.261 + SOME (_, eq) => Conv.rewr_conv eq
13.262 + | NONE => Conv.all_conv) ct
13.263 +in
13.264 +fun add_abs_min_max_rules ctxt thms =
13.265 + if Config.get ctxt unfold_defs
13.266 + then map (Conv.fconv_rule (More_Conv.bottom_conv unfold_conv ctxt)) thms
13.267 + else map fst (map_filter (AList.lookup (op =) defs) (add_syms thms)) @ thms
13.268 +end
13.269 +
13.270 +
13.271 +(* lift lambda terms into additional rules *)
13.272 +
13.273 +local
13.274 + val meta_eq = @{cpat "op =="}
13.275 + val meta_eqT = hd (Thm.dest_ctyp (Thm.ctyp_of_term meta_eq))
13.276 + fun inst_meta cT = Thm.instantiate_cterm ([(meta_eqT, cT)], []) meta_eq
13.277 + fun mk_meta_eq ct cu = Thm.mk_binop (inst_meta (Thm.ctyp_of_term ct)) ct cu
13.278 +
13.279 + fun lambda_conv conv =
13.280 + let
13.281 + fun sub_conv cvs ctxt ct =
13.282 + (case Thm.term_of ct of
13.283 + Const (@{const_name All}, _) $ Abs _ => quant_conv cvs ctxt
13.284 + | Const (@{const_name Ex}, _) $ Abs _ => quant_conv cvs ctxt
13.285 + | Const _ $ Abs _ => Conv.arg_conv (at_lambda_conv cvs ctxt)
13.286 + | Const (@{const_name Let}, _) $ _ $ Abs _ => Conv.combination_conv
13.287 + (Conv.arg_conv (sub_conv cvs ctxt)) (abs_conv cvs ctxt)
13.288 + | Abs _ => at_lambda_conv cvs ctxt
13.289 + | _ $ _ => Conv.comb_conv (sub_conv cvs ctxt)
13.290 + | _ => Conv.all_conv) ct
13.291 + and abs_conv cvs = Conv.abs_conv (fn (cv, cx) => sub_conv (cv::cvs) cx)
13.292 + and quant_conv cvs ctxt = Conv.arg_conv (abs_conv cvs ctxt)
13.293 + and at_lambda_conv cvs ctxt = abs_conv cvs ctxt then_conv conv cvs ctxt
13.294 + in sub_conv [] end
13.295 +
13.296 + fun used_vars cvs ct =
13.297 + let
13.298 + val lookup = AList.lookup (op aconv) (map (` Thm.term_of) cvs)
13.299 + val add = (fn (SOME ct) => insert (op aconvc) ct | _ => I)
13.300 + in Term.fold_aterms (add o lookup) (Thm.term_of ct) [] end
13.301 +
13.302 + val rev_int_fst_ord = rev_order o int_ord o pairself fst
13.303 + fun ordered_values tab =
13.304 + Termtab.fold (fn (_, x) => OrdList.insert rev_int_fst_ord x) tab []
13.305 + |> map snd
13.306 +in
13.307 +fun lift_lambdas ctxt thms =
13.308 + let
13.309 + val declare_frees = fold (Thm.fold_terms Term.declare_term_frees)
13.310 + val names = ref (declare_frees thms (Name.make_context []))
13.311 + val fresh_name = change_result names o yield_singleton Name.variants
13.312 +
13.313 + val defs = ref (Termtab.empty : (int * thm) Termtab.table)
13.314 + fun add_def t thm = change defs (Termtab.update (t, (serial (), thm)))
13.315 + fun make_def cvs eq = Thm.symmetric (fold norm_meta_def cvs eq)
13.316 + fun def_conv cvs ctxt ct =
13.317 + let
13.318 + val cvs' = used_vars cvs ct
13.319 + val ct' = fold Thm.cabs cvs' ct
13.320 + in
13.321 + (case Termtab.lookup (!defs) (Thm.term_of ct') of
13.322 + SOME (_, eq) => make_def cvs' eq
13.323 + | NONE =>
13.324 + let
13.325 + val {t, T, ...} = Thm.rep_cterm ct'
13.326 + val eq = mk_meta_eq (cert ctxt (Free (fresh_name "", T))) ct'
13.327 + val thm = Thm.assume eq
13.328 + in (add_def t thm; make_def cvs' thm) end)
13.329 + end
13.330 + val thms' = map (Conv.fconv_rule (lambda_conv def_conv ctxt)) thms
13.331 + val eqs = ordered_values (!defs)
13.332 + in
13.333 + (maps (#hyps o Thm.crep_thm) eqs, map (normalize_rule ctxt) eqs @ thms')
13.334 + end
13.335 +end
13.336 +
13.337 +
13.338 +(* make application explicit for functions with varying number of arguments *)
13.339 +
13.340 +local
13.341 + val const = prefix "c" and free = prefix "f"
13.342 + fun min i (e as (_, j)) = if i <> j then (true, Int.min (i, j)) else e
13.343 + fun add t i = Symtab.map_default (t, (false, i)) (min i)
13.344 + fun traverse t =
13.345 + (case Term.strip_comb t of
13.346 + (Const (n, _), ts) => add (const n) (length ts) #> fold traverse ts
13.347 + | (Free (n, _), ts) => add (free n) (length ts) #> fold traverse ts
13.348 + | (Abs (_, _, u), ts) => fold traverse (u :: ts)
13.349 + | (_, ts) => fold traverse ts)
13.350 + val prune = (fn (n, (true, i)) => Symtab.update (n, i) | _ => I)
13.351 + fun prune_tab tab = Symtab.fold prune tab Symtab.empty
13.352 +
13.353 + fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
13.354 + fun nary_conv conv1 conv2 ct =
13.355 + (Conv.combination_conv (nary_conv conv1 conv2) conv2 else_conv conv1) ct
13.356 + fun abs_conv conv tb = Conv.abs_conv (fn (cv, cx) =>
13.357 + let val n = fst (Term.dest_Free (Thm.term_of cv))
13.358 + in conv (Symtab.update (free n, 0) tb) cx end)
13.359 + val apply_rule = @{lemma "f x == apply f x" by (simp add: apply_def)}
13.360 +in
13.361 +fun explicit_application ctxt thms =
13.362 + let
13.363 + fun sub_conv tb ctxt ct =
13.364 + (case Term.strip_comb (Thm.term_of ct) of
13.365 + (Const (n, _), ts) => app_conv tb (const n) (length ts) ctxt
13.366 + | (Free (n, _), ts) => app_conv tb (free n) (length ts) ctxt
13.367 + | (Abs _, ts) => nary_conv (abs_conv sub_conv tb ctxt) (sub_conv tb ctxt)
13.368 + | (_, ts) => nary_conv Conv.all_conv (sub_conv tb ctxt)) ct
13.369 + and app_conv tb n i ctxt =
13.370 + (case Symtab.lookup tb n of
13.371 + NONE => nary_conv Conv.all_conv (sub_conv tb ctxt)
13.372 + | SOME j => apply_conv tb ctxt (i - j))
13.373 + and apply_conv tb ctxt i ct = (
13.374 + if i = 0 then nary_conv Conv.all_conv (sub_conv tb ctxt)
13.375 + else
13.376 + Conv.rewr_conv apply_rule then_conv
13.377 + binop_conv (apply_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct
13.378 +
13.379 + val tab = prune_tab (fold (traverse o Thm.prop_of) thms Symtab.empty)
13.380 + in map (Conv.fconv_rule (sub_conv tab ctxt)) thms end
13.381 +end
13.382 +
13.383 +
13.384 +(* combined normalization *)
13.385 +
13.386 +datatype config =
13.387 + RewriteTrivialLets |
13.388 + RewriteNegativeNumerals |
13.389 + RewriteNaturalNumbers |
13.390 + AddPairRules |
13.391 + AddFunUpdRules |
13.392 + AddAbsMinMaxRules
13.393 +
13.394 +fun normalize config ctxt thms =
13.395 + let fun if_enabled c f = member (op =) config c ? f ctxt
13.396 + in
13.397 + thms
13.398 + |> if_enabled RewriteTrivialLets trivial_let
13.399 + |> if_enabled RewriteNegativeNumerals positive_numerals
13.400 + |> if_enabled RewriteNaturalNumbers nat_as_int
13.401 + |> if_enabled AddPairRules add_pair_rules
13.402 + |> if_enabled AddFunUpdRules add_fun_upd_rules
13.403 + |> if_enabled AddAbsMinMaxRules add_abs_min_max_rules
13.404 + |> map (normalize_rule ctxt)
13.405 + |> lift_lambdas ctxt
13.406 + |> apsnd (explicit_application ctxt)
13.407 + end
13.408 +
13.409 +val setup = unfold_defs_setup
13.410 +
13.411 +end
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/HOL/SMT/Tools/smt_solver.ML Fri Sep 18 18:13:19 2009 +0200
14.3 @@ -0,0 +1,248 @@
14.4 +(* Title: HOL/SMT/Tools/smt_solver.ML
14.5 + Author: Sascha Boehme, TU Muenchen
14.6 +
14.7 +SMT solvers registry and SMT tactic.
14.8 +*)
14.9 +
14.10 +signature SMT_SOLVER =
14.11 +sig
14.12 + exception SMT_COUNTEREXAMPLE of bool * term list
14.13 +
14.14 + datatype interface = Interface of {
14.15 + normalize: SMT_Normalize.config list,
14.16 + translate: SMT_Translate.config }
14.17 +
14.18 + datatype proof_data = ProofData of {
14.19 + context: Proof.context,
14.20 + output: string list,
14.21 + recon: SMT_Translate.recon,
14.22 + assms: thm list option }
14.23 +
14.24 + datatype solver_config = SolverConfig of {
14.25 + name: {env_var: string, remote_name: string},
14.26 + interface: interface,
14.27 + arguments: string list,
14.28 + reconstruct: proof_data -> thm }
14.29 +
14.30 + (*options*)
14.31 + val timeout: int Config.T
14.32 + val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
14.33 + val trace: bool Config.T
14.34 + val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
14.35 +
14.36 + (*solvers*)
14.37 + type solver = Proof.context -> thm list -> thm
14.38 + type solver_info = Context.generic -> Pretty.T list
14.39 + val add_solver: string * (Proof.context -> solver_config) -> theory ->
14.40 + theory
14.41 + val all_solver_names_of: theory -> string list
14.42 + val add_solver_info: string * solver_info -> theory -> theory
14.43 + val solver_name_of: Context.generic -> string
14.44 + val select_solver: string -> Context.generic -> Context.generic
14.45 + val solver_of: Context.generic -> solver
14.46 +
14.47 + (*tactic*)
14.48 + val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
14.49 + val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic
14.50 +
14.51 + (*setup*)
14.52 + val setup: theory -> theory
14.53 + val print_setup: Context.generic -> unit
14.54 +end
14.55 +
14.56 +structure SMT_Solver: SMT_SOLVER =
14.57 +struct
14.58 +
14.59 +exception SMT_COUNTEREXAMPLE of bool * term list
14.60 +
14.61 +val theory_of = Context.cases I ProofContext.theory_of
14.62 +
14.63 +
14.64 +datatype interface = Interface of {
14.65 + normalize: SMT_Normalize.config list,
14.66 + translate: SMT_Translate.config }
14.67 +
14.68 +datatype proof_data = ProofData of {
14.69 + context: Proof.context,
14.70 + output: string list,
14.71 + recon: SMT_Translate.recon,
14.72 + assms: thm list option }
14.73 +
14.74 +datatype solver_config = SolverConfig of {
14.75 + name: {env_var: string, remote_name: string},
14.76 + interface: interface,
14.77 + arguments: string list,
14.78 + reconstruct: proof_data -> thm }
14.79 +
14.80 +
14.81 +(* SMT options *)
14.82 +
14.83 +val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" 30
14.84 +
14.85 +fun with_timeout ctxt f x =
14.86 + TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x
14.87 + handle TimeLimit.TimeOut => error ("SMT: timeout")
14.88 +
14.89 +val (trace, setup_trace) = Attrib.config_bool "smt_trace" false
14.90 +
14.91 +fun trace_msg ctxt f x =
14.92 + if Config.get ctxt trace then Output.tracing (f x) else ()
14.93 +
14.94 +
14.95 +(* interface to external solvers *)
14.96 +
14.97 +local
14.98 +
14.99 +fun with_tmp_files f x =
14.100 + let
14.101 + fun tmp_path () = File.tmp_path (Path.explode ("smt-" ^ serial_string ()))
14.102 + val in_path = tmp_path () and out_path = tmp_path ()
14.103 + val y = Exn.capture (f in_path out_path) x
14.104 + val _ = try File.rm in_path and _ = try File.rm out_path
14.105 + in Exn.release y end
14.106 +
14.107 +fun run in_path out_path (ctxt, cmd, output) =
14.108 + let
14.109 + val x = File.open_output output in_path
14.110 + val _ = trace_msg ctxt File.read in_path
14.111 +
14.112 + val _ = with_timeout ctxt system_out (cmd in_path out_path)
14.113 + fun lines_of path = the_default [] (try (File.fold_lines cons out_path) [])
14.114 + val ls = rev (dropwhile (equal "") (lines_of out_path))
14.115 + val _ = trace_msg ctxt cat_lines ls
14.116 + in (x, ls) end
14.117 +
14.118 +in
14.119 +
14.120 +fun run_solver ctxt {env_var, remote_name} args output =
14.121 + let
14.122 + val qf = File.shell_path and qq = enclose "'" "'"
14.123 + val path = getenv env_var and remote = getenv "REMOTE_SMT_SOLVER"
14.124 + fun cmd f1 f2 =
14.125 + if path <> ""
14.126 + then map qq (path :: args) @ [qf f1, ">", qf f2]
14.127 + else map qq (remote :: remote_name :: args) @ [qf f1, qf f2]
14.128 + in with_tmp_files run (ctxt, space_implode " " oo cmd, output) end
14.129 +
14.130 +end
14.131 +
14.132 +fun make_proof_data ctxt ((recon, thms), ls) =
14.133 + ProofData {context=ctxt, output=ls, recon=recon, assms=SOME thms}
14.134 +
14.135 +fun gen_solver solver ctxt prems =
14.136 + let
14.137 + val SolverConfig {name, interface, arguments, reconstruct} = solver ctxt
14.138 + val Interface {normalize=nc, translate=tc} = interface
14.139 + val thy = ProofContext.theory_of ctxt
14.140 + in
14.141 + SMT_Normalize.normalize nc ctxt prems
14.142 + ||> run_solver ctxt name arguments o SMT_Translate.translate tc thy
14.143 + ||> reconstruct o make_proof_data ctxt
14.144 + |-> fold SMT_Normalize.discharge_definition
14.145 + end
14.146 +
14.147 +
14.148 +(* solver store *)
14.149 +
14.150 +type solver = Proof.context -> thm list -> thm
14.151 +type solver_info = Context.generic -> Pretty.T list
14.152 +
14.153 +structure Solvers = TheoryDataFun
14.154 +(
14.155 + type T = ((Proof.context -> solver_config) * solver_info) Symtab.table
14.156 + val empty = Symtab.empty
14.157 + val copy = I
14.158 + val extend = I
14.159 + fun merge _ = Symtab.merge (K true)
14.160 + handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
14.161 +)
14.162 +
14.163 +val no_solver = "(none)"
14.164 +val add_solver = Solvers.map o Symtab.update_new o apsnd (rpair (K []))
14.165 +val all_solver_names_of = Symtab.keys o Solvers.get
14.166 +val lookup_solver = Symtab.lookup o Solvers.get
14.167 +fun add_solver_info (n, i) = Solvers.map (Symtab.map_entry n (apsnd (K i)))
14.168 +
14.169 +
14.170 +(* selected solver *)
14.171 +
14.172 +structure SelectedSolver = GenericDataFun
14.173 +(
14.174 + type T = serial * string
14.175 + val empty = (serial (), no_solver)
14.176 + val extend = I
14.177 + fun merge _ (sl1 as (s1, _), sl2 as (s2, _)) = if s1 > s2 then sl1 else sl2
14.178 +)
14.179 +
14.180 +val solver_name_of = snd o SelectedSolver.get
14.181 +
14.182 +fun select_solver name gen =
14.183 + if is_none (lookup_solver (theory_of gen) name)
14.184 + then error ("SMT solver not registered: " ^ quote name)
14.185 + else SelectedSolver.map (K (serial (), name)) gen
14.186 +
14.187 +fun raw_solver_of gen =
14.188 + (case lookup_solver (theory_of gen) (solver_name_of gen) of
14.189 + NONE => error "No SMT solver selected"
14.190 + | SOME (s, _) => s)
14.191 +
14.192 +val solver_of = gen_solver o raw_solver_of
14.193 +
14.194 +
14.195 +(* SMT tactic *)
14.196 +
14.197 +fun smt_unsat_tac solver ctxt rules =
14.198 + Tactic.rtac @{thm ccontr} THEN'
14.199 + SUBPROOF (fn {context, prems, ...} =>
14.200 + Tactic.rtac (solver context (rules @ prems)) 1) ctxt
14.201 +
14.202 +fun pretty_counterex ctxt (real, ex) =
14.203 + let
14.204 + val msg = if real then "Counterexample found:"
14.205 + else "Potential counterexample found:"
14.206 + val cex = if null ex then [Pretty.str "(no assignments)"]
14.207 + else map (Syntax.pretty_term ctxt) ex
14.208 + in Pretty.string_of (Pretty.big_list msg cex) end
14.209 +
14.210 +fun smt_tac' pass_smt_exns ctxt =
14.211 + let
14.212 + val solver = solver_of (Context.Proof ctxt)
14.213 + fun safe_solver ctxt thms = solver ctxt thms
14.214 + handle SMT_COUNTEREXAMPLE cex => error (pretty_counterex ctxt cex)
14.215 + val solver' = if pass_smt_exns then solver else safe_solver
14.216 + in smt_unsat_tac solver' ctxt end
14.217 +
14.218 +val smt_tac = smt_tac' false
14.219 +
14.220 +
14.221 +(* setup *)
14.222 +
14.223 +val setup =
14.224 + Attrib.setup (Binding.name "smt_solver")
14.225 + (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
14.226 + (Thm.declaration_attribute o K o select_solver))
14.227 + "SMT solver configuration" #>
14.228 + setup_timeout #>
14.229 + setup_trace
14.230 +
14.231 +fun print_setup gen =
14.232 + let
14.233 + val t = string_of_int (Config.get_generic gen timeout)
14.234 + val names = sort string_ord (all_solver_names_of (theory_of gen))
14.235 + val ns = if null names then [no_solver] else names
14.236 + val take_info = (fn (_, []) => NONE | info => SOME info)
14.237 + val infos =
14.238 + theory_of gen
14.239 + |> Symtab.dest o Solvers.get
14.240 + |> map_filter (fn (n, (_, info)) => take_info (n, info gen))
14.241 + |> sort (prod_ord string_ord (K EQUAL))
14.242 + |> map (fn (n, ps) => Pretty.big_list (n ^ ":") ps)
14.243 + in
14.244 + Pretty.writeln (Pretty.big_list "SMT setup:" [
14.245 + Pretty.str ("Current SMT solver: " ^ solver_name_of gen),
14.246 + Pretty.str_list "Available SMT solvers: " "" ns,
14.247 + Pretty.str ("Current timeout: " ^ t ^ " seconds"),
14.248 + Pretty.big_list "Solver-specific settings:" infos])
14.249 + end
14.250 +
14.251 +end
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/HOL/SMT/Tools/smt_translate.ML Fri Sep 18 18:13:19 2009 +0200
15.3 @@ -0,0 +1,507 @@
15.4 +(* Title: HOL/SMT/Tools/smt_translate.ML
15.5 + Author: Sascha Boehme, TU Muenchen
15.6 +
15.7 +Translate theorems into an SMT intermediate format and serialize them,
15.8 +depending on an SMT interface.
15.9 +*)
15.10 +
15.11 +signature SMT_TRANSLATE =
15.12 +sig
15.13 + (* intermediate term structure *)
15.14 + datatype sym =
15.15 + SConst of string * typ |
15.16 + SFree of string * typ |
15.17 + SNum of int * typ
15.18 + datatype squant = SForall | SExists
15.19 + datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
15.20 + datatype ('a, 'b) sterm =
15.21 + SVar of int |
15.22 + SApp of 'a * ('a, 'b) sterm list |
15.23 + SLet of (string * 'b) * ('a, 'b) sterm * ('a, 'b) sterm |
15.24 + SQuant of squant * (string * 'b) list * ('a, 'b) sterm spattern list *
15.25 + ('a, 'b) sterm
15.26 +
15.27 + (* table for built-in symbols *)
15.28 + type builtin_fun = typ -> (sym, typ) sterm list ->
15.29 + (string * (sym, typ) sterm list) option
15.30 + type builtin_table = (typ * builtin_fun) list Symtab.table
15.31 + val builtin_make: (term * string) list -> builtin_table
15.32 + val builtin_add: term * builtin_fun -> builtin_table -> builtin_table
15.33 + val builtin_lookup: builtin_table -> theory -> string * typ ->
15.34 + (sym, typ) sterm list -> (string * (sym, typ) sterm list) option
15.35 + val bv_rotate: (int -> string) -> builtin_fun
15.36 + val bv_extend: (int -> string) -> builtin_fun
15.37 + val bv_extract: (int -> int -> string) -> builtin_fun
15.38 +
15.39 + (* configuration options *)
15.40 + datatype prefixes = Prefixes of {
15.41 + var_prefix: string,
15.42 + typ_prefix: string,
15.43 + fun_prefix: string,
15.44 + pred_prefix: string }
15.45 + datatype markers = Markers of {
15.46 + term_marker: string,
15.47 + formula_marker: string }
15.48 + datatype builtins = Builtins of {
15.49 + builtin_typ: typ -> string option,
15.50 + builtin_num: int * typ -> string option,
15.51 + builtin_fun: bool -> builtin_table }
15.52 + datatype sign = Sign of {
15.53 + typs: string list,
15.54 + funs: (string * (string list * string)) list,
15.55 + preds: (string * string list) list }
15.56 + datatype config = Config of {
15.57 + strict: bool,
15.58 + prefixes: prefixes,
15.59 + markers: markers,
15.60 + builtins: builtins,
15.61 + serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit}
15.62 + datatype recon = Recon of {typs: typ Symtab.table, terms: term Symtab.table}
15.63 +
15.64 + val translate: config -> theory -> thm list -> TextIO.outstream ->
15.65 + recon * thm list
15.66 +
15.67 + val dest_binT: typ -> int
15.68 + val dest_funT: int -> typ -> typ list * typ
15.69 +end
15.70 +
15.71 +structure SMT_Translate: SMT_TRANSLATE =
15.72 +struct
15.73 +
15.74 +(* Intermediate term structure *)
15.75 +
15.76 +datatype sym =
15.77 + SConst of string * typ |
15.78 + SFree of string * typ |
15.79 + SNum of int * typ
15.80 +datatype squant = SForall | SExists
15.81 +datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
15.82 +datatype ('a, 'b) sterm =
15.83 + SVar of int |
15.84 + SApp of 'a * ('a, 'b) sterm list |
15.85 + SLet of (string * 'b) * ('a, 'b) sterm * ('a, 'b) sterm |
15.86 + SQuant of squant * (string * 'b) list * ('a, 'b) sterm spattern list *
15.87 + ('a, 'b) sterm
15.88 +
15.89 +fun app c ts = SApp (c, ts)
15.90 +
15.91 +fun map_pat f (SPat ps) = SPat (map f ps)
15.92 + | map_pat f (SNoPat ps) = SNoPat (map f ps)
15.93 +
15.94 +fun fold_map_pat f (SPat ps) = fold_map f ps #>> SPat
15.95 + | fold_map_pat f (SNoPat ps) = fold_map f ps #>> SNoPat
15.96 +
15.97 +val make_sconst = SConst o Term.dest_Const
15.98 +
15.99 +
15.100 +(* General type destructors. *)
15.101 +
15.102 +fun dest_binT T =
15.103 + (case T of
15.104 + Type (@{type_name "Numeral_Type.num0"}, _) => 0
15.105 + | Type (@{type_name "Numeral_Type.num1"}, _) => 1
15.106 + | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
15.107 + | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
15.108 + | _ => raise TYPE ("dest_binT", [T], []))
15.109 +
15.110 +val dest_wordT = (fn
15.111 + Type (@{type_name "word"}, [T]) => dest_binT T
15.112 + | T => raise TYPE ("dest_wordT", [T], []))
15.113 +
15.114 +val dest_funT =
15.115 + let
15.116 + fun dest Ts 0 T = (rev Ts, T)
15.117 + | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
15.118 + | dest _ _ T = raise TYPE ("dest_funT", [T], [])
15.119 + in dest [] end
15.120 +
15.121 +
15.122 +(* Table for built-in symbols *)
15.123 +
15.124 +type builtin_fun = typ -> (sym, typ) sterm list ->
15.125 + (string * (sym, typ) sterm list) option
15.126 +type builtin_table = (typ * builtin_fun) list Symtab.table
15.127 +
15.128 +fun builtin_make entries =
15.129 + let
15.130 + fun dest (t, bn) =
15.131 + let val (n, T) = Term.dest_Const t
15.132 + in (n, (Logic.varifyT T, K (SOME o pair bn))) end
15.133 + in Symtab.make (AList.group (op =) (map dest entries)) end
15.134 +
15.135 +fun builtin_add (t, f) tab =
15.136 + let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t)
15.137 + in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end
15.138 +
15.139 +fun builtin_lookup tab thy (n, T) ts =
15.140 + AList.lookup (Sign.typ_instance thy) (Symtab.lookup_list tab n) T
15.141 + |> (fn SOME f => f T ts | NONE => NONE)
15.142 +
15.143 +local
15.144 + val dest_nat = (fn
15.145 + SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i
15.146 + | _ => NONE)
15.147 +in
15.148 +fun bv_rotate mk_name T ts =
15.149 + dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts))
15.150 +
15.151 +fun bv_extend mk_name T ts =
15.152 + (case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of
15.153 + (SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE
15.154 + | _ => NONE)
15.155 +
15.156 +fun bv_extract mk_name T ts =
15.157 + (case (try dest_wordT (body_type T), dest_nat (hd ts)) of
15.158 + (SOME i, SOME lb) => SOME (mk_name (i + lb - 1) lb, tl ts)
15.159 + | _ => NONE)
15.160 +end
15.161 +
15.162 +
15.163 +(* Configuration options *)
15.164 +
15.165 +datatype prefixes = Prefixes of {
15.166 + var_prefix: string,
15.167 + typ_prefix: string,
15.168 + fun_prefix: string,
15.169 + pred_prefix: string }
15.170 +datatype markers = Markers of {
15.171 + term_marker: string,
15.172 + formula_marker: string }
15.173 +datatype builtins = Builtins of {
15.174 + builtin_typ: typ -> string option,
15.175 + builtin_num: int * typ -> string option,
15.176 + builtin_fun: bool -> builtin_table }
15.177 +datatype sign = Sign of {
15.178 + typs: string list,
15.179 + funs: (string * (string list * string)) list,
15.180 + preds: (string * string list) list }
15.181 +datatype config = Config of {
15.182 + strict: bool,
15.183 + prefixes: prefixes,
15.184 + markers: markers,
15.185 + builtins: builtins,
15.186 + serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit}
15.187 +datatype recon = Recon of {typs: typ Symtab.table, terms: term Symtab.table}
15.188 +
15.189 +
15.190 +(* Translate Isabelle/HOL terms into SMT intermediate terms.
15.191 + We assume that lambda-lifting has been performed before, i.e., lambda
15.192 + abstractions occur only at quantifiers and let expressions.
15.193 +*)
15.194 +local
15.195 + val quantifier = (fn
15.196 + @{const_name All} => SOME SForall
15.197 + | @{const_name Ex} => SOME SExists
15.198 + | _ => NONE)
15.199 +
15.200 + fun group_quant qname vs (t as Const (q, _) $ Abs (n, T, u)) =
15.201 + if q = qname then group_quant qname ((n, T) :: vs) u else (vs, t)
15.202 + | group_quant qname vs t = (vs, t)
15.203 +
15.204 + fun dest_trigger (@{term trigger} $ tl $ t) = (HOLogic.dest_list tl, t)
15.205 + | dest_trigger t = ([], t)
15.206 +
15.207 + fun pat f ps (Const (@{const_name pat}, _) $ p) = SPat (rev (f p :: ps))
15.208 + | pat f ps (Const (@{const_name nopat}, _) $ p) = SNoPat (rev (f p :: ps))
15.209 + | pat f ps (Const (@{const_name andpat}, _) $ p $ t) = pat f (f p :: ps) t
15.210 + | pat _ _ t = raise TERM ("pat", [t])
15.211 +
15.212 + fun trans Ts t =
15.213 + (case Term.strip_comb t of
15.214 + (t1 as Const (qn, qT), [t2 as Abs (n, T, t3)]) =>
15.215 + (case quantifier qn of
15.216 + SOME q =>
15.217 + let
15.218 + val (vs, u) = group_quant qn [(n, T)] t3
15.219 + val Us = map snd vs @ Ts
15.220 + val (ps, b) = dest_trigger u
15.221 + in SQuant (q, rev vs, map (pat (trans Us) []) ps, trans Us b) end
15.222 + | NONE => raise TERM ("intermediate", [t]))
15.223 + | (Const (@{const_name Let}, _), [t1, Abs (n, T, t2)]) =>
15.224 + SLet ((n, T), trans Ts t1, trans (T :: Ts) t2)
15.225 + | (Const (c as (@{const_name distinct}, _)), [t1]) =>
15.226 + (* this is not type-correct, but will be corrected at a later stage *)
15.227 + SApp (SConst c, map (trans Ts) (HOLogic.dest_list t1))
15.228 + | (Const c, ts) =>
15.229 + (case try HOLogic.dest_number t of
15.230 + SOME (T, i) => SApp (SNum (i, T), [])
15.231 + | NONE => SApp (SConst c, map (trans Ts) ts))
15.232 + | (Free c, ts) => SApp (SFree c, map (trans Ts) ts)
15.233 + | (Bound i, []) => SVar i
15.234 + | _ => raise TERM ("intermediate", [t]))
15.235 +in
15.236 +fun intermediate ts = map (trans [] o HOLogic.dest_Trueprop) ts
15.237 +end
15.238 +
15.239 +
15.240 +(* Separate formulas from terms by adding special marker symbols ("term",
15.241 + "formula"). Atoms "P" whose head symbol also occurs as function symbol are
15.242 + rewritten to "term P = term True". Connectives and built-in predicates
15.243 + occurring at term level are replaced by new constants, and theorems
15.244 + specifying their meaning are added.
15.245 +*)
15.246 +local
15.247 + (** Add the marker symbols "term" and "formulas" to separate formulas and
15.248 + terms. **)
15.249 +
15.250 + val connectives = map make_sconst [@{term True}, @{term False},
15.251 + @{term Not}, @{term "op &"}, @{term "op |"}, @{term "op -->"},
15.252 + @{term "op = :: bool => _"}]
15.253 +
15.254 + fun note false c (ps, fs) = (insert (op =) c ps, fs)
15.255 + | note true c (ps, fs) = (ps, insert (op =) c fs)
15.256 +
15.257 + val term_marker = SConst (@{const_name term}, Term.dummyT)
15.258 + val formula_marker = SConst (@{const_name formula}, Term.dummyT)
15.259 + fun mark f true t = f true t #>> app term_marker o single
15.260 + | mark f false t = f false t #>> app formula_marker o single
15.261 + fun mark' f false t = f true t #>> app term_marker o single
15.262 + | mark' f true t = f true t
15.263 + val mark_term = app term_marker o single
15.264 + fun lift_term_marker c ts =
15.265 + let val rem = (fn SApp (SConst (@{const_name term}, _), [t]) => t | t => t)
15.266 + in mark_term (SApp (c, map rem ts)) end
15.267 + fun is_term (SApp (SConst (@{const_name term}, _), _)) = true
15.268 + | is_term _ = false
15.269 +
15.270 + fun either x = (fn y as SOME _ => y | _ => x)
15.271 + fun get_loc loc i t =
15.272 + (case t of
15.273 + SVar j => if i = j then SOME loc else NONE
15.274 + | SApp (SConst (@{const_name term}, _), us) => get_locs true i us
15.275 + | SApp (SConst (@{const_name formula}, _), us) => get_locs false i us
15.276 + | SApp (_, us) => get_locs loc i us
15.277 + | SLet (_, u1, u2) => either (get_loc true i u1) (get_loc loc (i+1) u2)
15.278 + | SQuant (_, vs, _, u) => get_loc loc (i + length vs) u)
15.279 + and get_locs loc i ts = fold (either o get_loc loc i) ts NONE
15.280 +
15.281 + fun sep loc t =
15.282 + (case t of
15.283 + SVar i => pair t
15.284 + | SApp (c as SConst (@{const_name If}, _), u :: us) =>
15.285 + mark sep false u ##>> fold_map (sep loc) us #>> app c o (op ::)
15.286 + | SApp (c, us) =>
15.287 + if not loc andalso member (op =) connectives c
15.288 + then fold_map (sep loc) us #>> app c
15.289 + else note loc c #> fold_map (mark' sep loc) us #>> app c
15.290 + | SLet (v, u1, u2) =>
15.291 + sep loc u2 #-> (fn u2' =>
15.292 + mark sep (the (get_loc loc 0 u2')) u1 #>> (fn u1' =>
15.293 + SLet (v, u1', u2')))
15.294 + | SQuant (q, vs, ps, u) =>
15.295 + fold_map (fold_map_pat (mark sep true)) ps ##>>
15.296 + sep loc u #>> (fn (ps', u') =>
15.297 + SQuant (q, vs, ps', u')))
15.298 +
15.299 + (** Rewrite atoms. **)
15.300 +
15.301 + val unterm_rule = @{lemma "term x == x" by (simp add: term_def)}
15.302 + val unterm_conv = More_Conv.top_sweep_conv (K (Conv.rewr_conv unterm_rule))
15.303 +
15.304 + val dest_word_type = (fn Type (@{type_name word}, [T]) => T | T => T)
15.305 + fun instantiate [] _ = I
15.306 + | instantiate (v :: _) T =
15.307 + Term.subst_TVars [(v, dest_word_type (Term.domain_type T))]
15.308 +
15.309 + fun dest_alls (Const (@{const_name All}, _) $ Abs (_, _, t)) = dest_alls t
15.310 + | dest_alls t = t
15.311 + val dest_iff = (fn (Const (@{const_name iff}, _) $ t $ _ ) => t | t => t)
15.312 + val dest_eq = (fn (Const (@{const_name "op ="}, _) $ t $ _ ) => t | t => t)
15.313 + val dest_not = (fn (@{term Not} $ t) => t | t => t)
15.314 + val head_of = HOLogic.dest_Trueprop #> dest_alls #> dest_iff #> dest_not #>
15.315 + dest_eq #> Term.head_of
15.316 +
15.317 + fun prepare ctxt thm =
15.318 + let
15.319 + val rule = Conv.fconv_rule (unterm_conv ctxt) thm
15.320 + val prop = Thm.prop_of thm
15.321 + val inst = instantiate (Term.add_tvar_names prop [])
15.322 + fun inst_for T = (singleton intermediate (inst T prop), rule)
15.323 + in (make_sconst (head_of (Thm.prop_of rule)), inst_for) end
15.324 +
15.325 + val logicals = map (prepare @{context})
15.326 + @{lemma
15.327 + "~ holds False"
15.328 + "ALL p. holds (~ p) iff (~ holds p)"
15.329 + "ALL p q. holds (p & q) iff (holds p & holds q)"
15.330 + "ALL p q. holds (p | q) iff (holds p | holds q)"
15.331 + "ALL p q. holds (p --> q) iff (holds p --> holds q)"
15.332 + "ALL p q. holds (p iff q) iff (holds p iff holds q)"
15.333 + "ALL p q. holds (p = q) iff (p = q)"
15.334 + "ALL (a::int) b. holds (a < b) iff (a < b)"
15.335 + "ALL (a::int) b. holds (a <= b) iff (a <= b)"
15.336 + "ALL (a::real) b. holds (a < b) iff (a < b)"
15.337 + "ALL (a::real) b. holds (a <= b) iff (a <= b)"
15.338 + "ALL (a::'a::len0 word) b. holds (a < b) iff (a < b)"
15.339 + "ALL (a::'a::len0 word) b. holds (a <= b) iff (a <= b)"
15.340 + "ALL a b. holds (a <s b) iff (a <s b)"
15.341 + "ALL a b. holds (a <=s b) iff (a <=s b)"
15.342 + by (simp_all add: term_def iff_def)}
15.343 +
15.344 + fun is_instance thy (SConst (n, T), SConst (m, U)) =
15.345 + (n = m) andalso Sign.typ_instance thy (T, U)
15.346 + | is_instance _ _ = false
15.347 +
15.348 + fun lookup_logical thy (c as SConst (_, T)) =
15.349 + AList.lookup (is_instance thy) logicals c
15.350 + |> Option.map (fn inst_for => inst_for T)
15.351 + | lookup_logical _ _ = NONE
15.352 +
15.353 + val s_eq = make_sconst @{term "op = :: bool => _"}
15.354 + val s_True = mark_term (SApp (make_sconst @{term True}, []))
15.355 + fun holds (SApp (c, ts)) = SApp (s_eq, [lift_term_marker c ts, s_True])
15.356 + | holds t = SApp (s_eq, [mark_term t, s_True])
15.357 +
15.358 + val rewr_iff = (fn
15.359 + SConst (@{const_name "op ="}, T as @{typ "bool => bool => bool"}) =>
15.360 + SConst (@{const_name iff}, T)
15.361 + | c => c)
15.362 +
15.363 + fun rewrite ls =
15.364 + let
15.365 + fun rewr env loc t =
15.366 + (case t of
15.367 + SVar i => if not loc andalso nth env i then holds t else t
15.368 + | SApp (c as SConst (@{const_name term}, _), [u]) =>
15.369 + SApp (c, [rewr env true u])
15.370 + | SApp (c as SConst (@{const_name formula}, _), [u]) =>
15.371 + SApp (c, [rewr env false u])
15.372 + | SApp (c, us) =>
15.373 + let val f = if not loc andalso member (op =) ls c then holds else I
15.374 + in f (SApp (rewr_iff c, map (rewr env loc) us)) end
15.375 + | SLet (v, u1, u2) =>
15.376 + SLet (v, rewr env loc u1, rewr (is_term u1 :: env) loc u2)
15.377 + | SQuant (q, vs, ps, u) =>
15.378 + let val e = replicate (length vs) true @ env
15.379 + in SQuant (q, vs, map (map_pat (rewr e loc)) ps, rewr e loc u) end)
15.380 + in map (rewr [] false) end
15.381 +in
15.382 +fun separate thy ts =
15.383 + let
15.384 + val (ts', (ps, fs)) = fold_map (sep false) ts ([], [])
15.385 + val eq_name = (fn
15.386 + (SConst (n, _), SConst (m, _)) => n = m
15.387 + | (SFree (n, _), SFree (m, _)) => n = m
15.388 + | _ => false)
15.389 + val ls = filter (member eq_name fs) ps
15.390 + val (us, thms) = split_list (map_filter (lookup_logical thy) fs)
15.391 + in (thms, us @ rewrite ls ts') end
15.392 +end
15.393 +
15.394 +
15.395 +(* Collect the signature of intermediate terms, identify built-in symbols,
15.396 + rename uninterpreted symbols and types, make bound variables unique.
15.397 + We require @{term distinct} to be a built-in constant of the SMT solver.
15.398 +*)
15.399 +local
15.400 + fun empty_nctxt p = (p, 1)
15.401 + fun make_nctxt (pT, pf, pp) = (empty_nctxt pT, empty_nctxt (pf, pp))
15.402 + fun fresh_name (p, i) = (p ^ string_of_int i, (p, i+1))
15.403 + fun fresh_typ (nT, nfp) = fresh_name nT ||> (fn nT' => (nT', nfp))
15.404 + fun fresh_fun loc (nT, ((pf, pp), i)) =
15.405 + let val p = if loc then pf else pp
15.406 + in fresh_name (p, i) ||> (fn (_, i') => (nT, ((pf, pp), i'))) end
15.407 +
15.408 + val empty_sign = (Typtab.empty, Termtab.empty, Termtab.empty)
15.409 + fun lookup_typ (typs, _, _) = Typtab.lookup typs
15.410 + fun lookup_fun true (_, funs, _) = Termtab.lookup funs
15.411 + | lookup_fun false (_, _, preds) = Termtab.lookup preds
15.412 + fun add_typ x (typs, funs, preds) = (Typtab.update x typs, funs, preds)
15.413 + fun add_fun true x (typs, funs, preds) = (typs, Termtab.update x funs, preds)
15.414 + | add_fun false x (typs, funs, preds) = (typs, funs, Termtab.update x preds)
15.415 + fun make_sign (typs, funs, preds) = Sign {
15.416 + typs = map snd (Typtab.dest typs),
15.417 + funs = map snd (Termtab.dest funs),
15.418 + preds = map (apsnd fst o snd) (Termtab.dest preds) }
15.419 + fun make_rtab (typs, funs, preds) =
15.420 + let
15.421 + val rTs = Typtab.dest typs |> map swap |> Symtab.make
15.422 + val rts = Termtab.dest funs @ Termtab.dest preds
15.423 + |> map (apfst fst o swap) |> Symtab.make
15.424 + in Recon {typs=rTs, terms=rts} end
15.425 +
15.426 + fun either f g x = (case f x of NONE => g x | y => y)
15.427 +
15.428 + fun rep_typ (Builtins {builtin_typ, ...}) T (st as (vars, ns, sgn)) =
15.429 + (case either builtin_typ (lookup_typ sgn) T of
15.430 + SOME n => (n, st)
15.431 + | NONE =>
15.432 + let val (n, ns') = fresh_typ ns
15.433 + in (n, (vars, ns', add_typ (T, n) sgn)) end)
15.434 +
15.435 + fun rep_var bs (n, T) (vars, ns, sgn) =
15.436 + let val (n', vars') = fresh_name vars
15.437 + in (vars', ns, sgn) |> rep_typ bs T |>> pair n' end
15.438 +
15.439 + fun rep_fun bs loc t T i (st as (_, _, sgn0)) =
15.440 + (case lookup_fun loc sgn0 t of
15.441 + SOME (n, _) => (n, st)
15.442 + | NONE =>
15.443 + let
15.444 + val (Us, U) = dest_funT i T
15.445 + val (uns, (vars, ns, sgn)) =
15.446 + st |> fold_map (rep_typ bs) Us ||>> rep_typ bs U
15.447 + val (n, ns') = fresh_fun loc ns
15.448 + in (n, (vars, ns', add_fun loc (t, (n, uns)) sgn)) end)
15.449 +
15.450 + fun rep_num (bs as Builtins {builtin_num, ...}) (i, T) st =
15.451 + (case builtin_num (i, T) of
15.452 + SOME n => (n, st)
15.453 + | NONE => rep_fun bs true (HOLogic.mk_number T i) T 0 st)
15.454 +in
15.455 +fun signature_of prefixes markers builtins thy ts =
15.456 + let
15.457 + val Prefixes {var_prefix, typ_prefix, fun_prefix, pred_prefix} = prefixes
15.458 + val Markers {formula_marker, term_marker} = markers
15.459 + val Builtins {builtin_fun, ...} = builtins
15.460 +
15.461 + fun sign loc t =
15.462 + (case t of
15.463 + SVar i => pair (SVar i)
15.464 + | SApp (c as SConst (@{const_name term}, _), [u]) =>
15.465 + sign true u #>> app term_marker o single
15.466 + | SApp (c as SConst (@{const_name formula}, _), [u]) =>
15.467 + sign false u #>> app formula_marker o single
15.468 + | SApp (SConst (c as (_, T)), ts) =>
15.469 + (case builtin_lookup (builtin_fun loc) thy c ts of
15.470 + SOME (n, ts') => fold_map (sign loc) ts' #>> app n
15.471 + | NONE =>
15.472 + rep_fun builtins loc (Const c) T (length ts) ##>>
15.473 + fold_map (sign loc) ts #>> SApp)
15.474 + | SApp (SFree (c as (_, T)), ts) =>
15.475 + rep_fun builtins loc (Free c) T (length ts) ##>>
15.476 + fold_map (sign loc) ts #>> SApp
15.477 + | SApp (SNum n, _) => rep_num builtins n #>> (fn n => SApp (n, []))
15.478 + | SLet (v, u1, u2) =>
15.479 + rep_var builtins v #-> (fn v' =>
15.480 + sign loc u1 ##>> sign loc u2 #>> (fn (u1', u2') =>
15.481 + SLet (v', u1', u2')))
15.482 + | SQuant (q, vs, ps, u) =>
15.483 + fold_map (rep_var builtins) vs ##>>
15.484 + fold_map (fold_map_pat (sign loc)) ps ##>>
15.485 + sign loc u #>> (fn ((vs', ps'), u') =>
15.486 + SQuant (q, vs', ps', u')))
15.487 + in
15.488 + (empty_nctxt var_prefix, make_nctxt (typ_prefix, fun_prefix, pred_prefix),
15.489 + empty_sign)
15.490 + |> fold_map (sign false) ts
15.491 + |> (fn (us, (_, _, sgn)) => (make_rtab sgn, (make_sign sgn, us)))
15.492 + end
15.493 +end
15.494 +
15.495 +
15.496 +(* Combination of all translation functions and invocation of serialization. *)
15.497 +
15.498 +fun translate config thy thms stream =
15.499 + let val Config {strict, prefixes, markers, builtins, serialize} = config
15.500 + in
15.501 + map Thm.prop_of thms
15.502 + |> SMT_Monomorph.monomorph thy
15.503 + |> intermediate
15.504 + |> (if strict then separate thy else pair [])
15.505 + ||>> signature_of prefixes markers builtins thy
15.506 + ||> (fn (sgn, ts) => serialize sgn ts stream)
15.507 + |> (fn ((thms', rtab), _) => (rtab, thms' @ thms))
15.508 + end
15.509 +
15.510 +end
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/HOL/SMT/Tools/smtlib_interface.ML Fri Sep 18 18:13:19 2009 +0200
16.3 @@ -0,0 +1,168 @@
16.4 +(* Title: HOL/SMT/Tools/smtlib_interface.ML
16.5 + Author: Sascha Boehme, TU Muenchen
16.6 +
16.7 +Interface to SMT solvers based on the SMT-LIB format.
16.8 +*)
16.9 +
16.10 +signature SMTLIB_INTERFACE =
16.11 +sig
16.12 + val basic_builtins: SMT_Translate.builtins
16.13 + val default_attributes: string list
16.14 + val gen_interface: SMT_Translate.builtins -> string list ->
16.15 + SMT_Solver.interface
16.16 + val interface: SMT_Solver.interface
16.17 +end
16.18 +
16.19 +structure SMTLIB_Interface: SMTLIB_INTERFACE =
16.20 +struct
16.21 +
16.22 +structure T = SMT_Translate
16.23 +
16.24 +
16.25 +(* built-in types, functions and predicates *)
16.26 +
16.27 +val builtin_typ = (fn
16.28 + @{typ int} => SOME "Int"
16.29 + | @{typ real} => SOME "Real"
16.30 + | _ => NONE)
16.31 +
16.32 +val builtin_num = (fn
16.33 + (i, @{typ int}) => SOME (string_of_int i)
16.34 + | (i, @{typ real}) => SOME (string_of_int i ^ ".0")
16.35 + | _ => NONE)
16.36 +
16.37 +val builtin_funcs = T.builtin_make [
16.38 + (@{term If}, "ite"),
16.39 + (@{term "uminus :: int => _"}, "~"),
16.40 + (@{term "plus :: int => _"}, "+"),
16.41 + (@{term "minus :: int => _"}, "-"),
16.42 + (@{term "times :: int => _"}, "*"),
16.43 + (@{term "uminus :: real => _"}, "~"),
16.44 + (@{term "plus :: real => _"}, "+"),
16.45 + (@{term "minus :: real => _"}, "-"),
16.46 + (@{term "times :: real => _"}, "*") ]
16.47 +
16.48 +val builtin_preds = T.builtin_make [
16.49 + (@{term True}, "true"),
16.50 + (@{term False}, "false"),
16.51 + (@{term Not}, "not"),
16.52 + (@{term "op &"}, "and"),
16.53 + (@{term "op |"}, "or"),
16.54 + (@{term "op -->"}, "implies"),
16.55 + (@{term "op iff"}, "iff"),
16.56 + (@{term If}, "if_then_else"),
16.57 + (@{term distinct}, "distinct"),
16.58 + (@{term "op ="}, "="),
16.59 + (@{term "op < :: int => _"}, "<"),
16.60 + (@{term "op <= :: int => _"}, "<="),
16.61 + (@{term "op < :: real => _"}, "<"),
16.62 + (@{term "op <= :: real => _"}, "<=") ]
16.63 +
16.64 +
16.65 +(* serialization *)
16.66 +
16.67 +fun wr s stream = (TextIO.output (stream, s); stream)
16.68 +fun wr_line f = f #> wr "\n"
16.69 +
16.70 +fun sep f = wr " " #> f
16.71 +fun par f = sep (wr "(" #> f #> wr ")")
16.72 +
16.73 +fun wr1 s = sep (wr s)
16.74 +fun wrn f n = (fn [] => wr1 n | ts => par (wr n #> fold f ts))
16.75 +fun ins s f = (fn [] => I | x::xs => f x #> fold (fn x => wr1 s #> f x) xs)
16.76 +
16.77 +val term_marker = "__term"
16.78 +val formula_marker = "__form"
16.79 +fun dest_marker (T.SApp ("__term", [t])) = SOME (true, t)
16.80 + | dest_marker (T.SApp ("__form", [t])) = SOME (false, t)
16.81 + | dest_marker _ = NONE
16.82 +
16.83 +val tvar = prefix "?"
16.84 +val fvar = prefix "$"
16.85 +
16.86 +fun wr_expr loc env t =
16.87 + (case t of
16.88 + T.SVar i => wr1 (nth env i)
16.89 + | T.SApp (n, ts) =>
16.90 + (case dest_marker t of
16.91 + SOME (loc', t') => wr_expr loc' env t'
16.92 + | NONE => wrn (wr_expr loc env) n ts)
16.93 + | T.SLet ((v, _), t1, t2) =>
16.94 + if loc then raise TERM ("SMTLIB: let expression in term", [])
16.95 + else
16.96 + let
16.97 + val (loc', t1') = the (dest_marker t1)
16.98 + val (kind, v') = if loc' then ("let", tvar v) else ("flet", fvar v)
16.99 + in
16.100 + par (wr kind #> par (wr v' #> wr_expr loc' env t1') #>
16.101 + wr_expr loc (v' :: env) t2)
16.102 + end
16.103 + | T.SQuant (q, vs, ps, b) =>
16.104 + let
16.105 + val wr_quant = wr o (fn T.SForall => "forall" | T.SExists => "exists")
16.106 + fun wr_var (n, s) = par (wr (tvar n) #> wr1 s)
16.107 +
16.108 + val wre = wr_expr loc (map (tvar o fst) (rev vs) @ env)
16.109 +
16.110 + fun wrp s ts = wr1 (":" ^ s ^ "{") #> ins "," wre ts #> wr1 "}"
16.111 + fun wr_pat (T.SPat ts) = wrp "pat" ts
16.112 + | wr_pat (T.SNoPat ts) = wrp "nopat" ts
16.113 + in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)
16.114 +
16.115 +fun serialize attributes (T.Sign {typs, funs, preds}) ts stream =
16.116 + let
16.117 + fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
16.118 + in
16.119 + stream
16.120 + |> wr_line (wr "(benchmark Isabelle")
16.121 + |> fold (wr_line o wr) attributes
16.122 + |> length typs > 0 ?
16.123 + wr_line (wr ":extrasorts" #> par (fold wr1 typs))
16.124 + |> length funs > 0 ? (
16.125 + wr_line (wr ":extrafuns (") #>
16.126 + fold (wr_decl o apsnd (fn (Ts, T) => Ts @ [T])) funs #>
16.127 + wr_line (wr " )"))
16.128 + |> length preds > 0 ? (
16.129 + wr_line (wr ":extrapreds (") #>
16.130 + fold wr_decl preds #>
16.131 + wr_line (wr " )"))
16.132 + |> fold (fn t => wr ":assumption" #> wr_line (wr_expr false [] t)) ts
16.133 + |> wr_line (wr ":formula true")
16.134 + |> wr_line (wr ")")
16.135 + |> K ()
16.136 + end
16.137 +
16.138 +
16.139 +(* SMT solver interface using the SMT-LIB input format *)
16.140 +
16.141 +val basic_builtins = T.Builtins {
16.142 + builtin_typ = builtin_typ,
16.143 + builtin_num = builtin_num,
16.144 + builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
16.145 +
16.146 +val default_attributes = [":logic AUFLIRA", ":status unknown"]
16.147 +
16.148 +fun gen_interface builtins attributes = SMT_Solver.Interface {
16.149 + normalize = [
16.150 + SMT_Normalize.RewriteTrivialLets,
16.151 + SMT_Normalize.RewriteNegativeNumerals,
16.152 + SMT_Normalize.RewriteNaturalNumbers,
16.153 + SMT_Normalize.AddAbsMinMaxRules,
16.154 + SMT_Normalize.AddPairRules,
16.155 + SMT_Normalize.AddFunUpdRules ],
16.156 + translate = T.Config {
16.157 + strict = true,
16.158 + prefixes = T.Prefixes {
16.159 + var_prefix = "x",
16.160 + typ_prefix = "T",
16.161 + fun_prefix = "uf_",
16.162 + pred_prefix = "up_" },
16.163 + markers = T.Markers {
16.164 + term_marker = term_marker,
16.165 + formula_marker = formula_marker },
16.166 + builtins = builtins,
16.167 + serialize = serialize attributes }}
16.168 +
16.169 +val interface = gen_interface basic_builtins default_attributes
16.170 +
16.171 +end
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/src/HOL/SMT/Tools/yices_solver.ML Fri Sep 18 18:13:19 2009 +0200
17.3 @@ -0,0 +1,52 @@
17.4 +(* Title: HOL/SMT/Tools/yices_solver.ML
17.5 + Author: Sascha Boehme, TU Muenchen
17.6 +
17.7 +Interface of the SMT solver Yices.
17.8 +*)
17.9 +
17.10 +signature YICES_SOLVER =
17.11 +sig
17.12 + val setup: theory -> theory
17.13 +end
17.14 +
17.15 +structure Yices_Solver: YICES_SOLVER =
17.16 +struct
17.17 +
17.18 +val solver_name = "yices"
17.19 +val env_var = "YICES_SOLVER"
17.20 +
17.21 +val options = ["--evidence", "--smtlib"]
17.22 +
17.23 +fun cex_kind true = "Counterexample"
17.24 + | cex_kind false = "Possible counterexample"
17.25 +
17.26 +fun raise_cex real ctxt rtab ls =
17.27 + let val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls)
17.28 + in error (Pretty.string_of p) end
17.29 +
17.30 +structure S = SMT_Solver
17.31 +
17.32 +fun core_oracle (SMT_Solver.ProofData {context, output, recon, ...}) =
17.33 + let
17.34 + val empty_line = (fn "" => true | _ => false)
17.35 + val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
17.36 + val (l, ls) = split_first (dropwhile empty_line output)
17.37 + in
17.38 + if String.isPrefix "unsat" l then @{cprop False}
17.39 + else if String.isPrefix "sat" l then raise_cex true context recon ls
17.40 + else if String.isPrefix "unknown" l then raise_cex false context recon ls
17.41 + else error (solver_name ^ " failed")
17.42 + end
17.43 +
17.44 +fun smtlib_solver oracle _ =
17.45 + SMT_Solver.SolverConfig {
17.46 + name = {env_var=env_var, remote_name=solver_name},
17.47 + interface = SMTLIB_Interface.interface,
17.48 + arguments = options,
17.49 + reconstruct = oracle }
17.50 +
17.51 +val setup =
17.52 + Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
17.53 + SMT_Solver.add_solver (solver_name, smtlib_solver oracle))
17.54 +
17.55 +end
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/src/HOL/SMT/Tools/z3_interface.ML Fri Sep 18 18:13:19 2009 +0200
18.3 @@ -0,0 +1,98 @@
18.4 +(* Title: HOL/SMT/Tools/z3_interface.ML
18.5 + Author: Sascha Boehme, TU Muenchen
18.6 +
18.7 +Interface to Z3 based on a relaxed version of SMT-LIB.
18.8 +*)
18.9 +
18.10 +signature Z3_INTERFACE =
18.11 +sig
18.12 + val interface: SMT_Solver.interface
18.13 +end
18.14 +
18.15 +structure Z3_Interface: Z3_INTERFACE =
18.16 +struct
18.17 +
18.18 +structure T = SMT_Translate
18.19 +
18.20 +fun mk_name1 n i = n ^ "[" ^ string_of_int i ^ "]"
18.21 +fun mk_name2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
18.22 +
18.23 +val builtin_typ = (fn
18.24 + @{typ int} => SOME "Int"
18.25 + | @{typ real} => SOME "Real"
18.26 + | Type (@{type_name word}, [T]) =>
18.27 + Option.map (mk_name1 "BitVec") (try T.dest_binT T)
18.28 + | _ => NONE)
18.29 +
18.30 +val builtin_num = (fn
18.31 + (i, @{typ int}) => SOME (string_of_int i)
18.32 + | (i, @{typ real}) => SOME (string_of_int i ^ ".0")
18.33 + | (i, Type (@{type_name word}, [T])) =>
18.34 + Option.map (mk_name1 ("bv" ^ string_of_int i)) (try T.dest_binT T)
18.35 + | _ => NONE)
18.36 +
18.37 +val builtin_funcs = T.builtin_make [
18.38 + (@{term If}, "ite"),
18.39 + (@{term "uminus :: int => _"}, "~"),
18.40 + (@{term "plus :: int => _"}, "+"),
18.41 + (@{term "minus :: int => _"}, "-"),
18.42 + (@{term "times :: int => _"}, "*"),
18.43 + (@{term "op div :: int => _"}, "div"),
18.44 + (@{term "op mod :: int => _"}, "mod"),
18.45 + (@{term "op rem"}, "rem"),
18.46 + (@{term "uminus :: real => _"}, "~"),
18.47 + (@{term "plus :: real => _"}, "+"),
18.48 + (@{term "minus :: real => _"}, "-"),
18.49 + (@{term "times :: real => _"}, "*"),
18.50 + (@{term "op / :: real => _"}, "/"),
18.51 + (@{term "bitNOT :: 'a::len0 word => _"}, "bvnot"),
18.52 + (@{term "op AND :: 'a::len0 word => _"}, "bvand"),
18.53 + (@{term "op OR :: 'a::len0 word => _"}, "bvor"),
18.54 + (@{term "op XOR :: 'a::len0 word => _"}, "bvxor"),
18.55 + (@{term "uminus :: 'a::len0 word => _"}, "bvneg"),
18.56 + (@{term "op + :: 'a::len0 word => _"}, "bvadd"),
18.57 + (@{term "op - :: 'a::len0 word => _"}, "bvsub"),
18.58 + (@{term "op * :: 'a::len0 word => _"}, "bvmul"),
18.59 + (@{term "op div :: 'a::len0 word => _"}, "bvudiv"),
18.60 + (@{term "op mod :: 'a::len0 word => _"}, "bvurem"),
18.61 + (@{term "op sdiv"}, "bvsdiv"),
18.62 + (@{term "op smod"}, "bvsmod"),
18.63 + (@{term "op srem"}, "bvsrem"),
18.64 + (@{term word_cat}, "concat"),
18.65 + (@{term bv_shl}, "bvshl"),
18.66 + (@{term bv_lshr}, "bvlshr"),
18.67 + (@{term bv_ashr}, "bvashr")]
18.68 + |> T.builtin_add (@{term slice}, T.bv_extract (mk_name2 "extract"))
18.69 + |> T.builtin_add (@{term ucast}, T.bv_extend (mk_name1 "zero_extend"))
18.70 + |> T.builtin_add (@{term scast}, T.bv_extend (mk_name1 "sign_extend"))
18.71 + |> T.builtin_add (@{term word_rotl}, T.bv_rotate (mk_name1 "rotate_left"))
18.72 + |> T.builtin_add (@{term word_rotr}, T.bv_rotate (mk_name1 "rotate_right"))
18.73 +
18.74 +val builtin_preds = T.builtin_make [
18.75 + (@{term True}, "true"),
18.76 + (@{term False}, "false"),
18.77 + (@{term Not}, "not"),
18.78 + (@{term "op &"}, "and"),
18.79 + (@{term "op |"}, "or"),
18.80 + (@{term "op -->"}, "implies"),
18.81 + (@{term "op iff"}, "iff"),
18.82 + (@{term If}, "if_then_else"),
18.83 + (@{term distinct}, "distinct"),
18.84 + (@{term "op ="}, "="),
18.85 + (@{term "op < :: int => _"}, "<"),
18.86 + (@{term "op <= :: int => _"}, "<="),
18.87 + (@{term "op < :: real => _"}, "<"),
18.88 + (@{term "op <= :: real => _"}, "<="),
18.89 + (@{term "op < :: 'a::len0 word => _"}, "bvult"),
18.90 + (@{term "op <= :: 'a::len0 word => _"}, "bvule"),
18.91 + (@{term word_sless}, "bvslt"),
18.92 + (@{term word_sle}, "bvsle")]
18.93 +
18.94 +val builtins = T.Builtins {
18.95 + builtin_typ = builtin_typ,
18.96 + builtin_num = builtin_num,
18.97 + builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
18.98 +
18.99 +val interface = SMTLIB_Interface.gen_interface builtins []
18.100 +
18.101 +end
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/HOL/SMT/Tools/z3_model.ML Fri Sep 18 18:13:19 2009 +0200
19.3 @@ -0,0 +1,159 @@
19.4 +(* Title: HOL/SMT/Tools/z3_model.ML
19.5 + Author: Sascha Boehme and Philipp Meyer, TU Muenchen
19.6 +
19.7 +Parser for counterexamples generated by Z3.
19.8 +*)
19.9 +
19.10 +signature Z3_MODEL =
19.11 +sig
19.12 + val parse_counterex: SMT_Translate.recon -> string list -> term list
19.13 +end
19.14 +
19.15 +structure Z3_Model: Z3_MODEL =
19.16 +struct
19.17 +
19.18 +(* parsing primitives *)
19.19 +
19.20 +fun lift f (x, y) = apsnd (pair x) (f y)
19.21 +fun lift' f v (x, y) = apsnd (rpair y) (f v x)
19.22 +
19.23 +fun $$ s = lift (Scan.$$ s)
19.24 +fun this s = lift (Scan.this_string s)
19.25 +
19.26 +fun par scan = $$ "(" |-- scan --| $$ ")"
19.27 +
19.28 +val digit = (fn
19.29 + "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
19.30 + "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
19.31 + "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
19.32 +
19.33 +val nat_num = Scan.repeat1 (Scan.some digit) >>
19.34 + (fn ds => fold (fn d => fn i => i * 10 + d) ds 0)
19.35 +val int_num = Scan.optional (Scan.$$ "-" >> K (fn i => ~i)) I :|--
19.36 + (fn sign => nat_num >> sign)
19.37 +
19.38 +val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
19.39 + member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
19.40 +val name = Scan.many1 is_char >> implode
19.41 +
19.42 +
19.43 +(* parsing counterexamples *)
19.44 +
19.45 +datatype context = Context of {
19.46 + ttab: term Symtab.table,
19.47 + nctxt: Name.context,
19.48 + vtab: term Inttab.table }
19.49 +
19.50 +fun make_context (ttab, nctxt, vtab) =
19.51 + Context {ttab=ttab, nctxt=nctxt, vtab=vtab}
19.52 +
19.53 +fun empty_context (SMT_Translate.Recon {terms, ...}) =
19.54 + let
19.55 + val ns = Symtab.fold (Term.add_free_names o snd) terms []
19.56 + val nctxt = Name.make_context ns
19.57 + in make_context (terms, nctxt, Inttab.empty) end
19.58 +
19.59 +fun map_context f (Context {ttab, nctxt, vtab}) =
19.60 + make_context (f (ttab, nctxt, vtab))
19.61 +
19.62 +fun fresh_name (cx as Context {nctxt, ...}) =
19.63 + let val (n, nctxt') = yield_singleton Name.variants "" nctxt
19.64 + in (n, map_context (fn (ttab, _, vtab) => (ttab, nctxt', vtab)) cx) end
19.65 +
19.66 +fun ident name (cx as Context {ttab, ...}) =
19.67 + (case Symtab.lookup ttab name of
19.68 + SOME t => (t, cx)
19.69 + | NONE =>
19.70 + let val (n, cx') = fresh_name cx
19.71 + in (Free (n, Term.dummyT), cx) end)
19.72 +
19.73 +fun set_value t i = map_context (fn (ttab, nctxt, vtab) =>
19.74 + (ttab, nctxt, Inttab.update (i, t) vtab))
19.75 +
19.76 +fun get_value T i (cx as Context {vtab, ...}) =
19.77 + (case Inttab.lookup vtab i of
19.78 + SOME t => (t, cx)
19.79 + | _ => cx |> fresh_name |-> (fn n =>
19.80 + let val t = Free (n, T)
19.81 + in set_value t i #> pair t end))
19.82 +
19.83 +
19.84 +fun space s = lift (Scan.many Symbol.is_ascii_blank) s
19.85 +fun spaced p = p --| space
19.86 +
19.87 +val key = spaced (lift name) #-> lift' ident
19.88 +val mapping = spaced (this "->")
19.89 +fun in_braces p = spaced ($$ "{") |-- p --| spaced ($$ "}")
19.90 +
19.91 +val bool_expr =
19.92 + this "true" >> K @{term True} ||
19.93 + this "false" >> K @{term False}
19.94 +
19.95 +fun number_expr T =
19.96 + let
19.97 + val num = lift int_num >> HOLogic.mk_number T
19.98 + fun frac n d = Const (@{const_name divide}, T --> T --> T) $ n $ d
19.99 + in num :|-- (fn n => Scan.optional ($$ "/" |-- num >> frac n) n) end
19.100 +
19.101 +val value = this "val!" |-- lift nat_num
19.102 +fun value_expr T = value #-> lift' (get_value T)
19.103 +
19.104 +val domT = Term.domain_type
19.105 +val ranT = Term.range_type
19.106 +fun const_array T t = Abs ("x", T, t)
19.107 +fun upd_array T ((a, t), u) =
19.108 + Const (@{const_name fun_upd}, [T, domT T, ranT T] ---> T) $ a $ t $ u
19.109 +fun array_expr T st = if not (can domT T) then Scan.fail st else st |> (
19.110 + par (spaced (this "const") |-- expr (ranT T)) >> const_array (domT T) ||
19.111 + par (spaced (this "store") |-- spaced (array_expr T) --
19.112 + expr (Term.domain_type T) -- expr (Term.range_type T)) >> upd_array T)
19.113 +
19.114 +and expr T st =
19.115 + spaced (bool_expr || number_expr T || value_expr T || array_expr T) st
19.116 +
19.117 +fun const_val t =
19.118 + let fun rep u = spaced value #-> apfst o set_value u #> pair []
19.119 + in
19.120 + if can HOLogic.dest_number t then rep t
19.121 + else if t = @{term TT} then rep @{term True}
19.122 + else expr (Term.fastype_of t) >> (fn u => [HOLogic.mk_eq (t, u)])
19.123 + end
19.124 +
19.125 +fun func_value T = mapping |-- expr T
19.126 +
19.127 +fun first_pat T =
19.128 + let
19.129 + fun args T = if not (can domT T) then Scan.succeed [] else
19.130 + expr (domT T) ::: args (ranT T)
19.131 + fun value ts = func_value (snd (SMT_Translate.dest_funT (length ts) T))
19.132 + in args T :-- value end
19.133 +
19.134 +fun func_pat (Ts, T) = fold_map expr Ts -- func_value T
19.135 +fun else_pat (Ts, T) =
19.136 + let fun else_arg T cx = cx |> fresh_name |>> (fn n => Free (n, T))
19.137 + in
19.138 + fold_map (lift' else_arg) Ts ##>>
19.139 + spaced (this "else") |-- func_value T
19.140 + end
19.141 +fun next_pats T (fts as (ts, _)) =
19.142 + let val Tps = SMT_Translate.dest_funT (length ts) T
19.143 + in Scan.repeat (func_pat Tps) @@@ (else_pat Tps >> single) >> cons fts end
19.144 +
19.145 +fun mk_def' f (ts, t) = HOLogic.mk_eq (Term.list_comb (f, ts), t)
19.146 +fun mk_def (Const (@{const_name apply}, _)) (u :: us, t) = mk_def' u (us, t)
19.147 + | mk_def f (ts, t) = mk_def' f (ts, t)
19.148 +fun func_pats t =
19.149 + let val T = Term.fastype_of t
19.150 + in first_pat T :|-- next_pats T >> map (mk_def t) end
19.151 +
19.152 +val assign =
19.153 + key --| mapping :|-- (fn t => in_braces (func_pats t) || const_val t)
19.154 +
19.155 +val cex = space |-- Scan.repeat assign
19.156 +
19.157 +fun parse_counterex recon ls =
19.158 + (empty_context recon, explode (cat_lines ls))
19.159 + |> Scan.catch (Scan.finite' Symbol.stopper (Scan.error cex))
19.160 + |> flat o fst
19.161 +
19.162 +end
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/src/HOL/SMT/Tools/z3_solver.ML Fri Sep 18 18:13:19 2009 +0200
20.3 @@ -0,0 +1,83 @@
20.4 +(* Title: HOL/SMT/Tools/z3_solver.ML
20.5 + Author: Sascha Boehme, TU Muenchen
20.6 +
20.7 +Interface of the SMT solver Z3.
20.8 +*)
20.9 +
20.10 +signature Z3_SOLVER =
20.11 +sig
20.12 + val proofs: bool Config.T
20.13 + val options: string Config.T
20.14 +
20.15 + val setup: theory -> theory
20.16 +end
20.17 +
20.18 +structure Z3_Solver: Z3_SOLVER =
20.19 +struct
20.20 +
20.21 +val solver_name = "z3"
20.22 +val env_var = "Z3_SOLVER"
20.23 +
20.24 +val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" false
20.25 +val (options, options_setup) = Attrib.config_string "z3_options" ""
20.26 +
20.27 +fun add xs ys = ys @ xs
20.28 +
20.29 +fun get_options ctxt =
20.30 + ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false"]
20.31 + |> Config.get ctxt proofs ? add ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
20.32 + |> add (space_explode " " (Config.get ctxt options))
20.33 +
20.34 +fun pretty_config context = [
20.35 + Pretty.str ("With proofs: " ^
20.36 + (if Config.get_generic context proofs then "true" else "false")),
20.37 + Pretty.str ("Options: " ^
20.38 + space_implode " " (get_options (Context.proof_of context))) ]
20.39 +
20.40 +fun cmdline_options ctxt =
20.41 + get_options ctxt
20.42 + |> add ["-smt"]
20.43 +
20.44 +fun raise_cex real recon ls =
20.45 + let val cex = Z3_Model.parse_counterex recon ls
20.46 + in raise SMT_Solver.SMT_COUNTEREXAMPLE (real, cex) end
20.47 +
20.48 +fun check_unsat recon output =
20.49 + let
20.50 + val raw = not o String.isPrefix "WARNING" orf String.isPrefix "ERROR"
20.51 + val (ls, l) = the_default ([], "") (try split_last (filter raw output))
20.52 + in
20.53 + if String.isPrefix "unsat" l then ls
20.54 + else if String.isPrefix "sat" l then raise_cex true recon ls
20.55 + else if String.isPrefix "unknown" l then raise_cex false recon ls
20.56 + else error (solver_name ^ " failed")
20.57 + end
20.58 +
20.59 +fun core_oracle (SMT_Solver.ProofData {output, recon, ...}) =
20.60 + check_unsat recon output
20.61 + |> K @{cprop False}
20.62 +
20.63 +(* FIXME
20.64 +fun prover (SMT_Solver.ProofData {context, output, recon, assms}) =
20.65 + check_unsat recon output
20.66 + |> Z3_Proof.reconstruct context assms recon
20.67 +*)
20.68 +
20.69 +fun solver oracle ctxt =
20.70 + let val with_proof = Config.get ctxt proofs
20.71 + in
20.72 + SMT_Solver.SolverConfig {
20.73 + name = {env_var=env_var, remote_name=solver_name},
20.74 + interface = Z3_Interface.interface,
20.75 + arguments = cmdline_options ctxt,
20.76 + reconstruct = (*FIXME:if with_proof then prover else*) oracle }
20.77 + end
20.78 +
20.79 +val setup =
20.80 + proofs_setup #>
20.81 + options_setup #>
20.82 + Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
20.83 + SMT_Solver.add_solver (solver_name, solver oracle)) #>
20.84 + SMT_Solver.add_solver_info (solver_name, pretty_config)
20.85 +
20.86 +end
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/src/HOL/SMT/etc/settings Fri Sep 18 18:13:19 2009 +0200
21.3 @@ -0,0 +1,13 @@
21.4 +ISABELLE_SMT="$COMPONENT"
21.5 +
21.6 +REMOTE_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/remote_smt.pl"
21.7 +
21.8 +REMOTE_SMT_URL="http://www4.in.tum.de/smt/smt"
21.9 +
21.10 +#
21.11 +# Paths to local SMT solvers:
21.12 +#
21.13 +# CVC_SOLVER=PATH
21.14 +# YICES_SOLVER=PATH
21.15 +# Z3_SOLVER=PATH
21.16 +
22.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
22.2 +++ b/src/HOL/SMT/lib/scripts/remote_smt.pl Fri Sep 18 18:13:19 2009 +0200
22.3 @@ -0,0 +1,43 @@
22.4 +#!/usr/bin/env perl -w
22.5 +#
22.6 +# Script to invoke remote SMT solvers.
22.7 +# Author: Sascha Böhme
22.8 +#
22.9 +
22.10 +use strict;
22.11 +use LWP;
22.12 +
22.13 +
22.14 +# environment
22.15 +
22.16 +my $remote_smt_url = $ENV{"REMOTE_SMT_URL"};
22.17 +
22.18 +
22.19 +# arguments
22.20 +
22.21 +my $solver = $ARGV[0];
22.22 +my @options = @ARGV[1 .. ($#ARGV - 2)];
22.23 +my $problem_file = $ARGV[-2];
22.24 +my $output_file = $ARGV[-1];
22.25 +
22.26 +
22.27 +# call solver
22.28 +
22.29 +my $agent = LWP::UserAgent->new;
22.30 +$agent->agent("SMT-Request");
22.31 +$agent->timeout(180);
22.32 +my $response = $agent->post($remote_smt_url, [
22.33 + "Solver" => $solver,
22.34 + "Options" => join(" ", @options),
22.35 + "Problem" => [$problem_file] ],
22.36 + "Content_Type" => "form-data");
22.37 +if (not $response->is_success) {
22.38 + print "HTTP-Error: " . $response->message . "\n";
22.39 + exit 1;
22.40 +}
22.41 +else {
22.42 + open(FILE, ">$output_file");
22.43 + print FILE $response->content;
22.44 + close(FILE);
22.45 +}
22.46 +